Best-effort hack to provide a meaningful name for anonymous bound universes.

This restores the old behaviour that was printing qualified global names as
a representation of anonymous bound universes, at the cost of a ugly hack.
Ideally this should be handled by the callers, but for the time being the
trade-off is probably OK.

2 files changed, 15 insertions, 10 deletions

diff --git a/engine/univNames.ml b/engine/univNames.ml
index a4a08ff18e..bdcad21a21 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -65,6 +65,11 @@ let subst_ubinder (subst,(ref,l as orig)) =
   let ref' = fst (Globnames.subst_global subst ref) in
   if ref == ref' then orig else ref', l
 
+let name_universe lvl =
+  (** Best-effort naming from the string representation of the level. This is
+      completely hackish and should be solved in upper layers instead. *)
+  try Name (Id.of_string_soft (Level.to_string lvl)) with _ -> Anonymous
+
 let discharge_ubinder (_,(ref,l)) =
   (** Expand polymorphic binders with the section context *)
   let info = Lib.section_segment_of_reference ref in
@@ -75,7 +80,7 @@ let discharge_ubinder (_,(ref,l)) =
     try
       let qid = Nametab.shortest_qualid_of_universe na in
       Name (snd (Libnames.repr_qualid qid))
-    with Not_found -> Anonymous
+    with Not_found -> name_universe lvl
   in
   let l = List.mapi map sec_inst @ l in
   Some (Lib.discharge_global ref, l)
@@ -99,7 +104,7 @@ let register_universe_binders ref ubinders =
   let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in
   let map lvl =
     try Name (LMap.find lvl revmap)
-    with Not_found -> Anonymous
+    with Not_found -> name_universe lvl
   in
   let ubinders = Array.map_to_list map (Instance.to_array univs) in
   if not (List.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref, ubinders))
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 22b998fab9..0f673acb79 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -42,10 +42,10 @@ bar@{u} = nat
          *)
 
 bar is universe polymorphic
-foo@{u Var(1) v} = 
-Type@{Var(1)} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1,Var(1)+1,v+1)}
-(* u Var(1) v |=  *)
+foo@{u Top.17 v} = 
+Type@{Top.17} -> Type@{v} -> Type@{u}
+     : Type@{max(u+1,Top.17+1,v+1)}
+(* u Top.17 v |=  *)
 
 foo is universe polymorphic
 Type@{i} -> Type@{j}
@@ -155,14 +155,14 @@ inmod@{u} -> Type@{v}
 (* u v |=  *)
 
 Applied.infunct is universe polymorphic
-axfoo@{i Var(1) Var(2)} : Type@{Var(1)} -> Type@{i}
-(* i Var(1) Var(2) |=  *)
+axfoo@{i Top.48 Top.49} : Type@{Top.48} -> Type@{i}
+(* i Top.48 Top.49 |=  *)
 
 axfoo is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo
-axbar@{i Var(1) Var(2)} : Type@{Var(2)} -> Type@{i}
-(* i Var(1) Var(2) |=  *)
+axbar@{i Top.48 Top.49} : Type@{Top.49} -> Type@{i}
+(* i Top.48 Top.49 |=  *)
 
 axbar is universe polymorphic
 Argument scope is [type_scope]