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.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/uState.mli')

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