diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index e49a57af39..5cb677d1c6 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -226,7 +226,7 @@ let start_proof id str goals terminator = let initial_state = { pid = id; terminator = Ephemeron.create terminator; - proof = Proof.start Evd.empty goals; + proof = Proof.start (Evd.from_env (Global.env ())) goals; endline_tactic = None; section_vars = None; strength = str; @@ -237,7 +237,7 @@ let start_dependent_proof id str goals terminator = let initial_state = { pid = id; terminator = Ephemeron.create terminator; - proof = Proof.dependent_start Evd.empty goals; + proof = Proof.dependent_start (Evd.from_env (Global.env ())) goals; endline_tactic = None; section_vars = None; strength = str; |