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

6 files changed, 8 insertions, 8 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 1dca04336f..35166def01 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -226,9 +226,9 @@ let end_of_stack = CondEndStack end_of_stack_kind
 
 let unfocused = is_last_focus end_of_stack_kind
 
-let start goals =
+let start sigma goals =
   let pr = {
-    proofview = Proofview.init goals ;
+    proofview = Proofview.init sigma goals ;
     focus_stack = [] ;
     shelf = [] ;
     given_up = [] } in
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 48333285d4..b9c3aa1b0a 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -53,7 +53,7 @@ val proof : proof ->
 
 (*** General proof functions ***)
 
-val start : (Environ.env * Term.types) list -> proof
+val start : Evd.evar_map -> (Environ.env * Term.types) list -> proof
 val initial_goals : proof -> (Term.constr * Term.types) list
 
 (* Returns [true] if the considered proof is completed, that is if no goal remain
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;
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 } =
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
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 86ec3a8357..106205552d 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -196,7 +196,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
     errorlabstrm "lemma_inversion"
     (str"Computed inversion goal was not closed in initial signature.");
   *)
-  let pf = Proof.start [invEnv,invGoal] in
+  let pf = Proof.start Evd.empty [invEnv,invGoal] in
   let pf =
     fst (Proof.run_tactic env (
       Tacticals.New.tclTHEN intro (Tacticals.New.onLastHypId inv_op)) pf)