From ab4d3bae45265d18357bacbdeeefb7018f1e58c5 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 22 Jul 2014 17:44:10 +0200
Subject: Proof_global.start_dependent_proof: properly threads the sigma
 through the telescope.

Allows for a more refined notion of dependently generated initial goals.---
 proofs/proofview.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'proofs/proofview.ml')

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 8df23a8bd9..1797f38f0f 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 }
 
-- 
cgit v1.2.3