Generate names for anonymous polymorphic universes

This should make the univbinders output test less fragile as it
depends less on the global counter (still used for universes from
section variables).

1 files changed, 1 insertions, 6 deletions

diff --git a/engine/uState.ml b/engine/uState.ml
index ff60a5f9d4..d4cb59da26 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -114,16 +114,11 @@ let constraints ctx = snd ctx.local
 
 let context ctx = ContextSet.to_context ctx.local
 
-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. *)
-  Id.of_string_soft (Level.to_string lvl)
-
 let compute_instance_binders inst 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 -> Name (name_universe lvl)
+    with Not_found -> Anonymous
   in
   Array.map map (Instance.to_array inst)