diff options
| author | Emilio Jesus Gallego Arias | 2019-02-24 20:40:34 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-17 12:30:13 +0200 |
| commit | 9b97d4368aa714aa5f0ae0a91bec7bab7eb1a394 (patch) | |
| tree | bf37b981e2e67599f4c20e05936e129418830006 /vernac/vernac.mllib | |
| parent | 873281c256fc33941d93044acc3db8eda0a148ee (diff) | |
[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.
Diffstat (limited to 'vernac/vernac.mllib')
| -rw-r--r-- | vernac/vernac.mllib | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 0749314301..d28eeb341d 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -14,9 +14,9 @@ Proof_using Egramcoq Metasyntax DeclareDef -Lemmas DeclareObl Canonical +Lemmas Class Auto_ind_decl Search |