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/inductive.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/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 9bbcf07f7e..30d96a22e0 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -594,7 +594,7 @@ let rec ienv_decompose_prod (env,_ as ienv) n c = | _ -> assert false let lambda_implicit_lift n a = - let level = Level.make (DirPath.make [Id.of_string "implicit"]) 0 in + let level = Level.make2 (DirPath.make [Id.of_string "implicit"]) (Level.Id.make 0) in let implicit_sort = mkType (Universe.make level) in let lambda_implicit a = mkLambda (Anonymous, implicit_sort, a) in iterate lambda_implicit n (lift n a) |