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.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/proofview.mli')

diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index c07613f672..2945fb7141 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -36,7 +36,7 @@ val proofview : proofview -> Goal.goal list * Evd.evar_map
 
 (* Initialises a proofview, the argument is a list of environement, 
    conclusion types, creating that many initial goals. *)
-val init : (Environ.env * Term.types) list -> proofview
+val init : Evd.evar_map -> (Environ.env * Term.types) list -> proofview
 
 (* Returns whether this proofview is finished or not. That is,
    if it has empty subgoals in the comb. There could still be unsolved
-- 
cgit v1.2.3