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, 2 insertions, 2 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index bc251d33de..7eb32f34a2 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -31,10 +31,10 @@ let proofview p =
 
 (* Initialises a proofview, the argument is a list of environement, 
    conclusion types, and optional names, creating that many initial goals. *)
-let init = 
+let init sigma =
   let rec aux = function
   | [] ->  { initial = [] ; 
-	     solution = Evd.empty ;
+	     solution = sigma ;
              comb = [];
 	   }
   | (env,typ)::l -> let { initial = ret ; solution = sol ; comb = comb } =