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 /stm | |
| 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 'stm')
| -rw-r--r-- | stm/stm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 89d95d0cc9..2fefb7fbb3 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1537,7 +1537,7 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_vernac_interp stop - ~proof:(pobject, Lemmas.default_info) st + ~proof:(pobject, Lemmas.default_lemma_info) st { verbose = false; indentation = 0; strlen = 0; expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in ignore(Future.join checked_proof); @@ -1677,7 +1677,7 @@ end = struct (* {{{ *) let pterm, _info = PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in - let proof = pterm, Lemmas.default_info in + let proof = pterm, Lemmas.default_lemma_info in (* We jump at the beginning since the kernel handles side effects by also * looking at the ones that happen to be present in the current env *) |