diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-27 20:47:43 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-27 20:47:43 +0200 |
commit | 663a8647bbc32e11243091de80f9953ed5fb7eff (patch) | |
tree | 7fba0a308daee7586221f752e233dd8fa9c8f5f5 /stm/lemmas.ml | |
parent | d4725f692a5f202ca4c5d6341b586b0e377f6973 (diff) | |
parent | a7ea32fbf3829d1ce39ce9cc24b71791727090c5 (diff) |
Merge branch 'v8.5'
Diffstat (limited to 'stm/lemmas.ml')
-rw-r--r-- | stm/lemmas.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 39f581082..a2e8fac05 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -487,9 +487,11 @@ let save_proof ?proof = function let ctx = Evd.evar_context_universe_context (fst universes) in Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes) | None -> + let pftree = Pfedit.get_pftreestate () in let id, k, typ = Pfedit.current_proof_statement () in + let universes = Proof.initial_euctx pftree in (* This will warn if the proof is complete *) - let pproofs, universes = + let pproofs, _univs = Proof_global.return_proof ~allow_partial:true () in let sec_vars = match Pfedit.get_used_variables(), pproofs with @@ -501,7 +503,8 @@ let save_proof ?proof = function Some (Environ.keep_hyps env (Idset.union ids_typ ids_def)) | _ -> None in let names = Pfedit.get_universe_binders () in - let binders, ctx = Evd.universe_context ?names (Evd.from_ctx universes) in + let evd = Evd.from_ctx universes in + let binders, ctx = Evd.universe_context ?names evd in Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None), (universes, Some binders)) in |