diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-21 00:16:34 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-05 10:01:21 +0100 |
| commit | e3cefca41b568b1e517313051a111b0416cd2594 (patch) | |
| tree | c21a1fbcc2cbd6fe41cfd691df2103ff1f445989 /kernel/indtypes.ml | |
| parent | 6899d3aa567436784a08af4e179c2ef1fa504a02 (diff) | |
Slight simplification of the code of primitive projection (in relation
to c71aa6b and 6ababf) so as to rely on generic functions rather than
re-doing the de Bruijn indices cooking locally.
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 = |