From 50361dc784c8967e7c4b254102e2cb21cb7e9f9e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 22 Jun 2020 12:55:47 +0200
Subject: Make compute_instance_binders internal to UState

---
 engine/uState.ml | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 2 deletions(-)

(limited to 'engine/uState.ml')

diff --git a/engine/uState.ml b/engine/uState.ml
index 25d7638686..ff60a5f9d4 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -114,12 +114,25 @@ 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)
+  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 +446,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
-- 
cgit v1.2.3


From ae1acfefe52937ea7e3a098137df032363051361 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 31 Mar 2020 15:10:32 +0200
Subject: 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).
---
 engine/uState.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

(limited to 'engine/uState.ml')

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