Merge PR #13415: Separate interning and pretyping of universes

Reviewed-by: mattam82

4 files changed, 19 insertions, 12 deletions

diff --git a/engine/uState.ml b/engine/uState.ml
index 103b552d86..0c994dfea0 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -341,12 +341,16 @@ let constrain_variables diff uctx =
   in
   { uctx with local = (univs, local); univ_variables = vars }
 
-let qualid_of_level uctx =
+let id_of_level uctx l =
+  try Some (Option.get (LMap.find l (snd uctx.names)).uname)
+  with Not_found | Option.IsNone ->
+    None
+
+let qualid_of_level uctx l =
   let map, map_rev = uctx.names in
-    fun l ->
-      try Some (Libnames.qualid_of_ident (Option.get (LMap.find l map_rev).uname))
-      with Not_found | Option.IsNone ->
-        UnivNames.qualid_of_level l
+  try Some (Libnames.qualid_of_ident (Option.get (LMap.find l map_rev).uname))
+  with Not_found | Option.IsNone ->
+    UnivNames.qualid_of_level map l
 
 let pr_uctx_level uctx l =
   match qualid_of_level uctx l with
diff --git a/engine/uState.mli b/engine/uState.mli
index bd3aac0d8b..442c29180c 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -209,4 +209,7 @@ val update_sigma_univs : t -> UGraph.t -> t
 val pr_uctx_level : t -> Univ.Level.t -> Pp.t
 val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid option
 
+(** Only looks in the local names, not in the nametab. *)
+val id_of_level : t -> Univ.Level.t -> Id.t option
+
 val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 2e15558db2..f5542cc0f7 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -12,15 +12,15 @@ open Names
 open Univ
 
 
-let qualid_of_level l =
+let qualid_of_level ctx l =
   match Level.name l with
   | Some qid  ->
-    (try Some (Nametab.shortest_qualid_of_universe qid)
+    (try Some (Nametab.shortest_qualid_of_universe (Id.Map.domain ctx) qid)
      with Not_found -> None)
   | None -> None
 
-let pr_with_global_universes l =
-  match qualid_of_level l with
+let pr_with_global_universes ctx l =
+  match qualid_of_level ctx l with
   | Some qid  -> Libnames.pr_qualid qid
   | None -> Level.pr l
 
diff --git a/engine/univNames.mli b/engine/univNames.mli
index 5f69d199b3..875c043032 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -10,9 +10,6 @@
 
 open Univ
 
-val pr_with_global_universes : Level.t -> Pp.t
-val qualid_of_level : Level.t -> Libnames.qualid option
-
 (** Local universe name <-> level mapping *)
 
 type universe_binders = Univ.Level.t Names.Id.Map.t
@@ -20,3 +17,6 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 val empty_binders : universe_binders
 
 type univ_name_list = Names.lname list
+
+val pr_with_global_universes : universe_binders -> Level.t -> Pp.t
+val qualid_of_level : universe_binders -> Level.t -> Libnames.qualid option