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).

1 files changed, 12 insertions, 0 deletions

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