diff options
Diffstat (limited to 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index d0a477431..291da4a98 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -26,7 +26,7 @@ open Util type proofview = Proofview_monad.proofview open Proofview_monad -type entry = (Term.constr * Term.types) list +type entry = (Term.constr * Term.types Univ.in_universe_context_set) list let proofview p = p.comb , p.solution @@ -42,7 +42,7 @@ let init sigma = let (e, _) = Term.destEvar econstr in let new_defs = Evd.merge_context_set Evd.univ_rigid new_defs ctx in let gl = Goal.build e in - let entry = (econstr, typ) :: ret in + let entry = (econstr, (typ, ctx)) :: ret in entry, { solution = new_defs; comb = gl::comb; } in fun l -> @@ -52,17 +52,18 @@ let init sigma = type telescope = | TNil - | TCons of Environ.env*Term.types*(Term.constr -> telescope) + | TCons of Environ.env * Term.types Univ.in_universe_context_set * (Term.constr -> telescope) let dependent_init = let rec aux sigma = function | TNil -> [], { solution = sigma; comb = []; } - | TCons (env, typ, t) -> + | TCons (env, (typ, ctx), t) -> let (sigma, econstr ) = Evarutil.new_evar sigma env typ in + let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in let ret, { solution = sol; comb = comb } = aux sigma (t econstr) in let (e, _) = Term.destEvar econstr in let gl = Goal.build e in - let entry = (econstr, typ) :: ret in + let entry = (econstr, (typ, ctx)) :: ret in entry, { solution = sol; comb = gl :: comb; } in fun sigma t -> |