diff options
| author | Emilio Jesus Gallego Arias | 2020-06-30 12:55:02 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-30 12:55:02 +0200 |
| commit | bffe3e8dcbb6019b30d32081f0b56eba30bf8be7 (patch) | |
| tree | b2884dfed06b740e2b4fd44ff7cec61ca716f906 /printing/printer.mli | |
| parent | c2b76962b407cac8de4465be1e77cf45ff5822d9 (diff) | |
| parent | ae1acfefe52937ea7e3a098137df032363051361 (diff) | |
Merge PR #11977: Generate default names for bound universes of polymorphic definitions
Reviewed-by: ejgallego
Reviewed-by: herbelin
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 12 |
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 |