diff options
| author | Emilio Jesus Gallego Arias | 2019-06-09 18:51:39 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-24 20:53:41 +0200 |
| commit | 599f61a45769d5938758e0fcbd479b9c8f493a58 (patch) | |
| tree | 07d471e5c84cd67898d04c2f760af77bad785985 /vernac/vernacentries.mli | |
| parent | 4fe8612fbfd1581b23bb4c813c900ab687797814 (diff) | |
[lemmas] Reify info for implicits, univ_decls, prepare for rec_thms.
Key information about an interactive lemma proof was stored as a
closure on an ad-hoc hook, then later made available to the hook
closing actions.
Instead, we put this information in the lemma state and incorporate
these declarations into the normal save path.
We prepare to put the information about rec_thms in the state too.
Diffstat (limited to 'vernac/vernacentries.mli')
| -rw-r--r-- | vernac/vernacentries.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index e46212ca1c..05de191214 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -22,7 +22,7 @@ val vernac_require : (** The main interpretation function of vernacular expressions *) val interp : ?verbosely:bool -> - ?proof:(Proof_global.proof_object * Lemmas.proof_info) -> + ?proof:(Proof_global.proof_object * Lemmas.lemma_info) -> st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t (** Prepare a "match" template for a given inductive type. |