Merge PR #9155: Fix race condition triggered by fresh universe generation

2 files changed, 20 insertions, 5 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 33ced6d6e0..ce7c7c8702 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -589,8 +589,23 @@ let detype_cofix detype avoid env sigma n (names,tys,bodies) =
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
 
+(* TODO use some algebraic type with a case for unnamed univs so we
+   can cleanly detype them. NB: this corresponds to a hack in
+   Pretyping.interp_universe_level_name to convert Foo.xx strings into
+   universes. *)
+let hack_qualid_of_univ_level sigma l =
+  match Termops.reference_of_level sigma l with
+  | Some qid -> qid
+  | None ->
+    let path = String.split_on_char '.' (Univ.Level.to_string l) in
+    let path = List.rev_map Id.of_string_soft path in
+    Libnames.qualid_of_dirpath (DirPath.make path)
+
 let detype_universe sigma u =
-  let fn (l, n) = Some (Termops.reference_of_level sigma l, n) in
+  let fn (l, n) =
+    let qid = hack_qualid_of_univ_level sigma l in
+    Some (qid, n)
+  in
   Univ.Universe.map fn u
 
 let detype_sort sigma = function
@@ -611,7 +626,7 @@ let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index
 let set_detype_anonymous f = detype_anonymous := f
 
 let detype_level sigma l =
-  let l = Termops.reference_of_level sigma l in
+  let l = hack_qualid_of_univ_level sigma l in
   GType (UNamed l)
 
 let detype_instance sigma l = 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f5e48bcd39..2be0f73ea4 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.(make (UGlobal.make dp num)) in
       let evd =
         try Evd.add_global_univ evd level
         with UGraph.AlreadyDeclared -> evd