Interactive elaborator doesn't save changes to global state

[david-christiansen]

When leaving the interactive elaborator, the changes to the global state (such as auxiliary definitions created during the process) are not kept for the rechecking phase, which leads to proof scripts that are correct but that Idris initially rejects. Putting them in the file makes them work again. For example, I have an induction tactic that lazily generates elimination principles for datatypes, and these eliminators are not around for the recheck phase.

[david-christiansen]

Interestingly, direct executions of context-modifying tactics work fine, but defining wrappers around them makes them not work.

[david-christiansen]

OK, this is fixed in my Elab branch - it'll get in next time I merge.