diff options
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index de97268b37..2ff4193384 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -734,7 +734,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params matching with a parameter context. *) let indty, paramsletsubst = (* [ty] = [Ind inst] is typed in context [params] *) - let inst = Context.Rel.to_extended_vect 0 paramslet in + let inst = Context.Rel.to_extended_vect mkRel 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 |