From d71f9b16a49ce4faa61ba9b3c57f43c3acceb8cb Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Mon, 4 Nov 2013 13:20:47 +0000
Subject: 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
---
 proofs/proofview.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs/proofview.ml')

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 } =
-- 
cgit v1.2.3