Merge PR #1033: Universe binder improvements

1 files changed, 6 insertions, 4 deletions

diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 89099a043f..8f3a6ddc47 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -31,9 +31,11 @@ val print_eval :
   reduction_function -> env -> Evd.evar_map ->
     Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
 
-val print_name : env -> Evd.evar_map -> reference or_by_notation -> Pp.t
+val print_name : env -> Evd.evar_map -> reference or_by_notation ->
+  Vernacexpr.univ_name_list option -> Pp.t
 val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t
-val print_about : env -> Evd.evar_map -> reference or_by_notation -> Pp.t
+val print_about : env -> Evd.evar_map -> reference or_by_notation ->
+  Vernacexpr.univ_name_list option -> Pp.t
 val print_impargs : reference or_by_notation -> Pp.t
 
 (** Pretty-printing functions for classes and coercions *)
@@ -80,8 +82,8 @@ val print_located_module : reference -> Pp.t
 val print_located_other : string -> reference -> Pp.t
 
 type object_pr = {
-  print_inductive           : MutInd.t -> Pp.t;
-  print_constant_with_infos : Constant.t -> Pp.t;
+  print_inductive           : MutInd.t -> Universes.univ_name_list option -> Pp.t;
+  print_constant_with_infos : Constant.t -> Universes.univ_name_list option -> Pp.t;
   print_section_variable    : env -> Evd.evar_map -> variable -> Pp.t;
   print_syntactic_def       : env -> KerName.t -> Pp.t;
   print_module              : bool -> ModPath.t -> Pp.t;