Merge PR #11977: Generate default names for bound universes of polymorphic definitions

Reviewed-by: ejgallego
Reviewed-by: herbelin

3 files changed, 11 insertions, 50 deletions

diff --git a/engine/uState.ml b/engine/uState.ml
index 25d7638686..d4cb59da26 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -114,12 +114,20 @@ let constraints ctx = snd ctx.local
 
 let context ctx = ContextSet.to_context ctx.local
 
+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 -> Anonymous
+  in
+  Array.map map (Instance.to_array inst)
+
 let univ_entry ~poly uctx =
   let open Entries in
   if poly then
     let (binders, _) = uctx.names in
     let uctx = context uctx in
-    let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in
+    let nas = compute_instance_binders (UContext.instance uctx) binders in
     Polymorphic_entry (nas, uctx)
   else Monomorphic_entry (context_set uctx)
 
@@ -433,7 +441,7 @@ let check_univ_decl ~poly uctx decl =
     if poly then
       let (binders, _) = uctx.names in
       let uctx = universe_context ~names ~extensible uctx in
-      let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in
+      let nas = compute_instance_binders (UContext.instance uctx) binders in
       Entries.Polymorphic_entry (nas, uctx)
     else
       let () = check_universe_context_set ~names ~extensible uctx in
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 6d9095680c..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,43 +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
 
-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)
-  in
-  Array.map map (Instance.to_array inst)
-
 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
diff --git a/engine/univNames.mli b/engine/univNames.mli
index 34a18d6b6e..5f69d199b3 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -19,15 +19,4 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 
 val empty_binders : universe_binders
 
-val compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t array
-
 type univ_name_list = Names.lname list
-
-(** [universe_binders_with_opt_names ref l]
-
-    If [l] is [Some univs] return the universe binders naming the bound levels
-    of [ref] by [univs] (skipping Anonymous). May error if the lengths mismatch.
-
-    Otherwise return the bound universe names registered for [ref]. *)
-val universe_binders_with_opt_names : AUContext.t ->
-  univ_name_list option -> universe_binders