Allow local universe renaming in Print.

2 files changed, 26 insertions, 0 deletions

diff --git a/engine/universes.ml b/engine/universes.ml
index 459c53002..194de2cee 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -35,6 +35,21 @@ let universe_binders_of_global ref : universe_binders =
 let register_universe_binders ref l =
   universe_binders_table := Refmap.add ref l !universe_binders_table
 
+type univ_name_list = Name.t Loc.located list
+
+let universe_binders_with_opt_names ref levels = function
+  | None -> universe_binders_of_global ref
+  | Some udecl ->
+    if Int.equal(List.length levels) (List.length udecl)
+    then
+      List.fold_left2 (fun acc (_,na) lvl -> match na with
+          | Anonymous -> acc
+          | Name na -> Names.Id.Map.add na lvl acc)
+        empty_binders udecl levels
+    else
+      CErrors.user_err ~hdr:"universe_binders_with_opt_names"
+        Pp.(str "Universe instance should have length " ++ int (List.length levels))
+
 (* To disallow minimization to Set *)
 
 let set_minimization = ref true
diff --git a/engine/universes.mli b/engine/universes.mli
index 621ca5e84..1401c4ee8 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -28,6 +28,17 @@ val empty_binders : universe_binders
 val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
 val universe_binders_of_global : Globnames.global_reference -> universe_binders
 
+type univ_name_list = Name.t Loc.located list
+
+(** [universe_binders_with_opt_names ref u l]
+
+    If [l] is [Some univs] return the universe binders naming the levels of [u] by [univs] (skipping Anonymous).
+    May error if the lengths mismatch.
+
+    Otherwise return [universe_binders_of_global ref]. *)
+val universe_binders_with_opt_names : Globnames.global_reference ->
+  Univ.Level.t list -> univ_name_list option -> universe_binders
+
 (** The global universe counter *)
 val set_remote_new_univ_level : Level.t RemoteCounter.installer