diff options
Diffstat (limited to 'kernel/indtypes.ml')
-rw-r--r-- | kernel/indtypes.ml | 12 |
1 files changed, 3 insertions, 9 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 21d1e7134..a649ec81e 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -695,18 +695,12 @@ 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 _, _, subst, inst = - List.fold_right - (fun (na, b, t) (i, j, subst, inst) -> - match b with - | None -> (i-1, j-1, mkRel i :: subst, mkRel j :: inst) - | Some b -> (i, j-1, substl subst b :: subst, inst)) - paramslet (nparamargs, List.length paramslet, [], []) - in + let inst = extended_rel_list 0 paramslet in + let subst = subst_of_rel_context_instance paramslet inst in let subst = (* For the record parameter: *) mkRel 1 :: List.map (lift 1) subst in - let ty = mkApp (mkIndU indu, CArray.rev_of_list inst) in + let ty = mkApp (mkIndU indu, Array.of_list inst) in ty, subst in let ci = |