From 40f6ecfaef5976e6955d6468844b782bc88e6280 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 2 Dec 2020 14:51:13 +0100
Subject: Delay inventing names for monomorphic universes

This avoids doing it repeatedly for nothing in intern/extern.
---
 engine/uState.ml  | 17 +----------------
 engine/uState.mli |  2 +-
 2 files changed, 2 insertions(+), 17 deletions(-)

(limited to 'engine')

diff --git a/engine/uState.ml b/engine/uState.ml
index 0eb8475958..20ea24dd87 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -157,23 +157,8 @@ let of_binders names =
   in
   { empty with names = (names, rev_map) }
 
-let invent_name (named,cnt) u =
-  let rec aux i =
-    let na = Id.of_string ("u"^(string_of_int i)) in
-    if Id.Map.mem na named then aux (i+1)
-    else Id.Map.add na u named, i+1
-  in
-  aux cnt
-
 let universe_binders uctx =
-  let named, rev = uctx.names in
-  let named, _ = LSet.fold (fun u named ->
-      match LMap.find u rev with
-      | exception Not_found -> (* not sure if possible *) invent_name named u
-      | { uname = None } -> invent_name named u
-      | { uname = Some _ } -> named)
-      (ContextSet.levels uctx.local) (named, 0)
-  in
+  let named, _ = uctx.names in
   named
 
 let instantiate_variable l b v =
diff --git a/engine/uState.mli b/engine/uState.mli
index 442c29180c..9cff988c99 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -79,7 +79,7 @@ val univ_entry : poly:bool -> t -> Entries.universes_entry
 (** Pick from {!context} or {!context_set} based on [poly]. *)
 
 val universe_binders : t -> UnivNames.universe_binders
-(** Return names of universes, inventing names if needed *)
+(** Return local names of universes. *)
 
 (** {5 Constraints handling} *)
 
-- 
cgit v1.2.3