From 7fa49442f30dceb7e403fb5dab660002dda7f6e9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 15 Dec 2015 15:25:30 +0100 Subject: Fixing e3cefca41b about supposingly simplifying primitive projections typing. Had built the instance for substitution in the wrong context. --- kernel/indtypes.ml | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index a649ec81e..11df40caf 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -681,6 +681,7 @@ let used_section_variables env inds = keep_hyps env ids let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) +let rel_list n m = Array.to_list (rel_vect n m) exception UndefinableExpansion @@ -695,12 +696,16 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params that typechecking projections requires just a substitution and not matching with a parameter context. *) let indty, paramsletsubst = - let inst = extended_rel_list 0 paramslet in - let subst = subst_of_rel_context_instance paramslet inst in + (* [ty] = [Ind inst] is typed in context [params] *) + let inst = extended_rel_vect 0 paramslet in + let ty = mkApp (mkIndU indu, inst) in + (* [Ind inst] is typed in context [params-wo-let] *) + let inst' = rel_list 0 nparamargs in + (* {params-wo-let |- subst:params] *) + let subst = subst_of_rel_context_instance paramslet inst' in + (* {params-wo-let, x:Ind inst' |- subst':(params,x:Ind inst)] *) let subst = (* For the record parameter: *) - mkRel 1 :: List.map (lift 1) subst - in - let ty = mkApp (mkIndU indu, Array.of_list inst) in + mkRel 1 :: List.map (lift 1) subst in ty, subst in let ci = -- cgit v1.2.3