Proof_global.start_dependent_proof: properly threads the sigma through the telescope.

Allows for a more refined notion of dependently generated initial goals.

6 files changed, 17 insertions, 17 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 3d5eb2031..60522c54b 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -237,8 +237,8 @@ let start sigma goals =
     shelf = [] ;
     given_up = [] } in
   _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr
-let dependent_start sigma goals =
-  let entry, proofview = Proofview.dependent_init sigma goals in
+let dependent_start goals =
+  let entry, proofview = Proofview.dependent_init goals in
   let pr = {
     proofview;
     entry;
diff --git a/proofs/proof.mli b/proofs/proof.mli
index a77b74124..be5311fed 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -52,7 +52,7 @@ val proof : proof ->
 (*** General proof functions ***)
 
 val start : Evd.evar_map -> (Environ.env * Term.types) list -> proof
-val dependent_start : Evd.evar_map -> Proofview.telescope -> proof
+val dependent_start : Proofview.telescope -> 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 8a3c0f775..5a7fb3ceb 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -235,11 +235,11 @@ let start_proof sigma id str goals terminator =
     mode = find_proof_mode "No" } in
   push initial_state pstates
 
-let start_dependent_proof sigma id str goals terminator =
+let start_dependent_proof id str goals terminator =
   let initial_state = {
     pid = id;
     terminator = Ephemeron.create terminator;
-    proof = Proof.dependent_start sigma goals;
+    proof = Proof.dependent_start goals;
     endline_tactic = None;
     section_vars = None;
     strength = str;
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index be01229c9..d8e84d0aa 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -84,7 +84,7 @@ val start_proof :
 (** Like [start_proof] except that there may be dependencies between
     initial goals. *)
 val start_dependent_proof :
-  Evd.evar_map -> Names.Id.t -> Decl_kinds.goal_kind -> Proofview.telescope  ->
+  Names.Id.t -> Decl_kinds.goal_kind -> Proofview.telescope  ->
     proof_terminator -> unit
 
 (* Takes a function to add to the exceptions data relative to the
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 8df23a8bd..1797f38f0 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -51,22 +51,22 @@ let init sigma =
     entry, { v with solution = Typeclasses.mark_unresolvables v.solution }
 
 type telescope =
-  | TNil
-  | TCons of Environ.env * Term.types * (Term.constr -> telescope)
+  | TNil of Evd.evar_map
+  | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope)
 
 let dependent_init =
-  let rec aux sigma = function
-  | TNil -> [], { solution = sigma; comb = []; }
-  | TCons (env, typ, t) ->
+  let rec aux = function
+  | TNil sigma -> [], { solution = sigma; comb = []; }
+  | TCons (env, sigma, typ, t) ->
     let (sigma, econstr ) = Evarutil.new_evar sigma env typ in
-    let ret, { solution = sol; comb = comb } = aux sigma (t econstr) in
+    let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
     let (e, _) = Term.destEvar econstr in
     let gl = Goal.build e in
     let entry = (econstr, typ) :: ret in
     entry, { solution = sol; comb = gl :: comb; }
   in
-  fun sigma t ->
-    let entry, v = aux sigma t in
+  fun t ->
+    let entry, v = aux t in
     (* Marks all the goal unresolvable for typeclasses. *)
     entry, { v with solution = Typeclasses.mark_unresolvables v.solution }
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 1aad0e090..b1447e8ba 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -40,13 +40,13 @@ type entry
 val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview
 
 type telescope =
-  | TNil
-  | TCons of Environ.env * Term.types * (Term.constr -> telescope)
+  | TNil of Evd.evar_map
+  | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope)
 
 (* Like [init], but goals are allowed to be depedenent on one
    another. Dependencies between goals is represented with the type
    [telescope] instead of [list]. *)
-val dependent_init  : Evd.evar_map -> telescope -> entry * proofview
+val dependent_init  : telescope -> entry * proofview
 
 (* Returns whether this proofview is finished or not. That is,
    if it has empty subgoals in the comb. There could still be unsolved