diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-18 17:04:12 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-18 21:22:11 +0100 |
| commit | 6ababf42b3f03926c30cfbd209436ec83a21769e (patch) | |
| tree | cdd1350661a5c78f2609eeb5f3c0f38b517b6118 /kernel/indtypes.ml | |
| parent | 0346ee4472711fc30b7cf197c1bad5c32140f831 (diff) | |
Fixing fix c71aa6b to primitive projections.
- Introduced an error: fold was counting in the wrong direction and I
did not test it. Sorry.
- Substitution from params-with-let to params-without-let was still
not correct.
Hopefully everything ok now. Eventually, we should use canonical
combinators for that: extended_rel_context to built the instance and
and a combinator apparently yet to define for building a substitution
contracting the let-ins.
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 6c32626ad..a46c33bf0 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -653,13 +653,13 @@ 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_i - (fun i (na, b, t) (subst, inst) -> + let _, _, subst, inst = + List.fold_right + (fun (na, b, t) (i, j, subst, inst) -> match b with - | None -> (mkRel i :: subst, mkRel i :: inst) - | Some b -> (substl subst b) :: subst, inst) - 1 paramslet ([], []) + | 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 subst = (* For the record parameter: *) mkRel 1 :: List.map (lift 1) subst |