diff options
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 8efda16d64..68d44f8782 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -218,7 +218,9 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : typ let check_subtyping cumi paramsctxt env_ar inds = let numparams = Context.Rel.nhyps paramsctxt in let uctx = CumulativityInfo.univ_context cumi in - let new_levels = Array.init (UContext.size uctx) (fun i -> Level.make2 DirPath.empty (Level.Id.make i)) in + let new_levels = Array.init (UContext.size uctx) + (fun i -> Level.make (Level.UGlobal.make DirPath.empty i)) + in let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap) LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels in |