get semanticsExtra building with new exceptions

Some of its theorems' conclusions are non-trivially different now, since
exception results can include values, and since evaluate can introduce
references to Bind, Div, and Eq (even though they might not be bound).
So we sometimes have an additional assumption that the cenv binds these;
and every_result etc. look inside exception results too.