From 78a8d59b39dfcb07b94721fdcfd9241d404905d2 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 15:30:02 +0100 Subject: Introducing contexts parameterized by the inner term type. This allows the decoupling of the notions of context containing kernel terms and context containing tactic-level terms. --- kernel/inductive.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 3c4c2796e..d8d365c34 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -297,7 +297,7 @@ let build_dependent_inductive ind (_,mip) params = applist (mkIndU ind, List.map (lift mip.mind_nrealdecls) params - @ Context.Rel.to_extended_list 0 realargs) + @ Context.Rel.to_extended_list mkRel 0 realargs) (* This exception is local *) exception LocalArity of (sorts_family * sorts_family * arity_error) option @@ -355,7 +355,7 @@ let build_branches_type (ind,u) (_,mip as specif) params p = let (lparams,vargs) = List.chop (inductive_params specif) allargs in let cargs = let cstr = ith_constructor_of_inductive ind (i+1) in - let dep_cstr = applist (mkConstructU (cstr,u),lparams@(Context.Rel.to_extended_list 0 cstrsign)) in + let dep_cstr = applist (mkConstructU (cstr,u),lparams@(Context.Rel.to_extended_list mkRel 0 cstrsign)) in vargs @ [dep_cstr] in let base = lambda_appvect_assum (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in it_mkProd_or_LetIn base cstrsign in -- cgit v1.2.3