From 280c922fc55b57c430cad721c83650a796a375fd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Wed, 20 Sep 2017 19:45:43 +0200
Subject: Allow local universe renaming in Print.

---
 engine/universes.ml | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'engine/universes.ml')

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
-- 
cgit v1.2.3