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 /interp | |
| 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 'interp')
| -rw-r--r-- | interp/declare.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index 1e972d3e35..0c9d26dd01 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -469,7 +469,7 @@ type universe_source = | QualifiedUniv of Id.t (* global universe introduced by some global value *) | UnqualifiedUniv (* other global universe *) -type universe_name_decl = universe_source * (Id.t * Nametab.universe_id) list +type universe_name_decl = universe_source * (Id.t * Univ.Level.Qualid.t) list let check_exists sp = if Nametab.exists_universe sp then @@ -543,9 +543,9 @@ let do_universe poly l = let l = List.map (fun {CAst.v=id} -> let lev = UnivGen.new_univ_id () in - (id, lev)) l + (id, Univ.Level.Qualid.make (Global.current_dirpath ()) lev)) l in - let ctx = List.fold_left (fun ctx (_,(dp,i)) -> Univ.LSet.add (Univ.Level.make dp i) ctx) + let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx) Univ.LSet.empty l, Univ.Constraint.empty in let () = declare_universe_context poly ctx in |