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, 24 deletions

diff --git a/engine/univNames.ml b/engine/univNames.ml
index 9a66386a21..2e15558db2 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Util
 open Names
 open Univ
 
@@ -30,30 +29,8 @@ let pr_with_global_universes l =
 
 (** Local universe names of polymorphic references *)
 
-type universe_binders = Univ.Level.t Names.Id.Map.t
+type universe_binders = Level.t Names.Id.Map.t
 
 let empty_binders = Id.Map.empty
 
 type univ_name_list = Names.lname list
-
-let universe_binders_with_opt_names orig names =
-  let orig = AUContext.names orig in
-  let orig = Array.to_list orig in
-  let udecl = match names with
-  | None -> orig
-  | Some udecl ->
-    try
-      List.map2 (fun orig {CAst.v = na} ->
-          match na with
-          | Anonymous -> orig
-          | Name id -> Name id) orig udecl
-    with Invalid_argument _ ->
-      let len = List.length orig in
-      CErrors.user_err ~hdr:"universe_binders_with_opt_names"
-        Pp.(str "Universe instance should have length " ++ int len)
-  in
-  let fold i acc na = match na with
-  | Name id -> Names.Id.Map.add id (Level.var i) acc
-  | Anonymous -> acc
-  in
-  List.fold_left_i fold 0 empty_binders udecl