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).
---
 printing/printer.mli | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'printing/printer.mli')

diff --git a/printing/printer.mli b/printing/printer.mli
index 8c633b5e79..8805819890 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -132,6 +132,18 @@ val pr_universes  : evar_map ->
   ?variance:Univ.Variance.t array -> ?priv:Univ.ContextSet.t ->
   Declarations.universes -> Pp.t
 
+(** [universe_binders_with_opt_names ref l]
+
+    If [l] is [Some univs] return the universe binders naming the
+   bound levels of [ref] by [univs] (generating names for Anonymous).
+   May error if the lengths mismatch.
+
+    Otherwise return the bound universe names registered for [ref].
+
+    Inefficient on large contexts due to name generation. *)
+val universe_binders_with_opt_names : Univ.AUContext.t ->
+  UnivNames.univ_name_list option -> UnivNames.universe_binders
+
 (** Printing global references using names as short as possible *)
 
 val pr_global_env          : Id.Set.t -> GlobRef.t -> Pp.t
-- 
cgit v1.2.3