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 /pretyping | |
| 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 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f5e48bcd39..d01c44811f 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -120,8 +120,8 @@ let interp_known_universe_level evd qid = if qualid_is_ident qid then Evd.universe_of_name evd @@ qualid_basename qid else raise Not_found with Not_found -> - let univ, k = Nametab.locate_universe qid in - Univ.Level.make univ k + let qid = Nametab.locate_universe qid in + Univ.Level.make qid let interp_universe_level_name ~anon_rigidity evd qid = try evd, interp_known_universe_level evd qid @@ -140,7 +140,7 @@ let interp_universe_level_name ~anon_rigidity evd qid = user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name" (Pp.(str "Undeclared global universe: " ++ Libnames.pr_qualid qid)) in - let level = Univ.Level.make dp num in + let level = Univ.Level.make2 dp (Univ.Level.Id.make num) in let evd = try Evd.add_global_univ evd level with UGraph.AlreadyDeclared -> evd |