[proof] Remove terminator type, unifying regular and obligation ones.

We radically redesign how proof closing information is stored. Instead
of a user-defined closure, we now reify control into a single data
structure containing the needed information.

In this scheme, the `Lemmas` module can get extra information with
obligation info when opening the proof, and will correspondingly call
the right closing function based on this.

This is the start of what could be a much bigger unification of all
the proof save paths.

0 files changed, 0 insertions, 0 deletions