diff options
| author | Maxime Dénès | 2018-12-04 10:33:47 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-12-06 11:09:27 +0100 |
| commit | 3e275d4bd1c3eb002b68c36ab116e5ab687d52f3 (patch) | |
| tree | 6ea705714c862ab019aa312daf42d40ca50a4ace /kernel/indtypes.ml | |
| parent | a2c8b7df8a0702ab716c0b97ad63d235b58b93a0 (diff) | |
Fix race condition triggered by fresh universe generation
Remote counters were trying to build universe levels (as opposed to
simple integers), but did not have access to the right dirpath at
construction time. We fix it by constructing the level only at use time,
and we introduce some abstractions for qualified and unqualified level
names.
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 a4a02791b4..8efda16d64 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -218,7 +218,7 @@ 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.make2 DirPath.empty (Level.Id.make 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 |