diff options
| author | Enrico Tassi | 2018-12-11 16:06:28 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2018-12-11 16:06:28 +0100 |
| commit | df657bd52d20b1c41e2ef4d44bde207323de6935 (patch) | |
| tree | 85fde4a47f00585dfae4bd09c27f3cf8cbef5526 /kernel/indtypes.ml | |
| parent | 97f5f37f782ffb9914fa8f67e745ba1effad20be (diff) | |
| parent | cff3c5a7148afc722852bd01658fe49ffec1d967 (diff) | |
Merge PR #9155: Fix race condition triggered by fresh universe generation
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 a4a02791b4..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) (Level.make DirPath.empty) 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 |