aboutsummaryrefslogtreecommitdiff
path: root/proofs/proof_global.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proof_global.ml')
-rw-r--r--proofs/proof_global.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index ac61f4e679..12a5285043 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -239,7 +239,7 @@ end
let start_proof id str goals ?(compute_guard=[]) hook =
let initial_state = {
pid = id;
- proof = Proof.start goals;
+ proof = Proof.start Evd.empty goals;
endline_tactic = None;
section_vars = None;
strength = str;