Allowing proofs starting with a non-empty evarmap.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17055 85f007b7-540e-0410-9357-904b9bb8a0f7

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;