remove the push/pop around typing, to ensure that inferred constants are properly kept in the typing env
properly distinguish the model from the newly defined constants, and thread the model appropriately to ensure that definitions are evaluated in the correct model (and not an empty one)
Two problems fixed here:
This should close #163