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 /engine/uState.ml | |
| parent | 97f5f37f782ffb9914fa8f67e745ba1effad20be (diff) | |
| parent | cff3c5a7148afc722852bd01658fe49ffec1d967 (diff) | |
Merge PR #9155: Fix race condition triggered by fresh universe generation
Diffstat (limited to 'engine/uState.ml')
| -rw-r--r-- | engine/uState.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index 6aecc368e6..185283225c 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -324,12 +324,14 @@ let constrain_variables diff ctx = let qualid_of_level uctx = let map, map_rev = uctx.uctx_names in fun l -> - try Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname) + try Some (Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname)) with Not_found | Option.IsNone -> UnivNames.qualid_of_level l let pr_uctx_level uctx l = - Libnames.pr_qualid (qualid_of_level uctx l) + match qualid_of_level uctx l with + | Some qid -> Libnames.pr_qualid qid + | None -> Univ.Level.pr l type ('a, 'b) gen_universe_decl = { univdecl_instance : 'a; (* Declared universes *) @@ -533,7 +535,7 @@ let emit_side_effects eff u = let new_univ_variable ?loc rigid name ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = - let u = UnivGen.new_univ_level () in + let u = UnivGen.fresh_level () in let ctx' = Univ.ContextSet.add_universe u ctx in let uctx', pred = match rigid with |