Allow local universe renaming in Print.

13 files changed, 189 insertions, 66 deletions

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 60cd8b73a..3ebeba178 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -10,6 +10,8 @@ defined object referred by {\qualid}.
 
 \begin{ErrMsgs}
 \item {\qualid} \errindex{not a defined object}
+\item \errindex{Universe instance should have length} $n$.
+\item \errindex{This object does not support universe names.}
 \end{ErrMsgs}
 
 \begin{Variants}
@@ -27,6 +29,11 @@ constructor, abbreviation, \ldots), long name, type, implicit
 arguments and argument scopes. It does not print the body of
 definitions or proofs.
 
+\item {\tt Print {\qualid}@\{names\}.}\\
+This locally renames the polymorphic universes of {\qualid}.
+An underscore means the raw universe is printed.
+This form can be used with {\tt Print Term} and {\tt About}.
+
 %\item {\tt Print Proof {\qualid}.}\comindex{Print Proof}\\
 %In case \qualid\ denotes an opaque theorem defined in a section,
 %it is stored on a special unprintable form and displayed as 
diff --git a/engine/universes.ml b/engine/universes.ml
index 459c53002..194de2cee 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -35,6 +35,21 @@ let universe_binders_of_global ref : universe_binders =
 let register_universe_binders ref l =
   universe_binders_table := Refmap.add ref l !universe_binders_table
 
+type univ_name_list = Name.t Loc.located list
+
+let universe_binders_with_opt_names ref levels = function
+  | None -> universe_binders_of_global ref
+  | Some udecl ->
+    if Int.equal(List.length levels) (List.length udecl)
+    then
+      List.fold_left2 (fun acc (_,na) lvl -> match na with
+          | Anonymous -> acc
+          | Name na -> Names.Id.Map.add na lvl acc)
+        empty_binders udecl levels
+    else
+      CErrors.user_err ~hdr:"universe_binders_with_opt_names"
+        Pp.(str "Universe instance should have length " ++ int (List.length levels))
+
 (* To disallow minimization to Set *)
 
 let set_minimization = ref true
diff --git a/engine/universes.mli b/engine/universes.mli
index 621ca5e84..1401c4ee8 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -28,6 +28,17 @@ val empty_binders : universe_binders
 val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
 val universe_binders_of_global : Globnames.global_reference -> universe_binders
 
+type univ_name_list = Name.t Loc.located list
+
+(** [universe_binders_with_opt_names ref u l]
+
+    If [l] is [Some univs] return the universe binders naming the levels of [u] by [univs] (skipping Anonymous).
+    May error if the lengths mismatch.
+
+    Otherwise return [universe_binders_of_global ref]. *)
+val universe_binders_with_opt_names : Globnames.global_reference ->
+  Univ.Level.t list -> univ_name_list option -> universe_binders
+
 (** The global universe counter *)
 val set_remote_new_univ_level : Level.t RemoteCounter.installer
 
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 9aef4b131..96bcba5e8 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -40,6 +40,8 @@ type goal_reference =
   | NthGoal of int
   | GoalId of Id.t
 
+type univ_name_list = Name.t Loc.located list
+
 type printable =
   | PrintTables
   | PrintFullContext
@@ -54,7 +56,7 @@ type printable =
   | PrintMLLoadPath
   | PrintMLModules
   | PrintDebugGC
-  | PrintName of reference or_by_notation
+  | PrintName of reference or_by_notation * univ_name_list option
   | PrintGraph
   | PrintClasses
   | PrintTypeClasses
@@ -70,7 +72,7 @@ type printable =
   | PrintScopes
   | PrintScope of string
   | PrintVisibility of string option
-  | PrintAbout of reference or_by_notation * goal_selector option
+  | PrintAbout of reference or_by_notation * univ_name_list option * goal_selector option
   | PrintImplicit of reference or_by_notation
   | PrintAssumptions of bool * bool * reference or_by_notation
   | PrintStrategy of reference or_by_notation option
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index a01ea26af..0e585cff7 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -875,7 +875,7 @@ GEXTEND Gram
 
       (* Printing (careful factorization of entries) *)
       | IDENT "Print"; p = printable -> VernacPrint p
-      | IDENT "Print"; qid = smart_global -> VernacPrint (PrintName qid)
+      | IDENT "Print"; qid = smart_global; l = OPT univ_name_list -> VernacPrint (PrintName (qid,l))
       | IDENT "Print"; IDENT "Module"; "Type"; qid = global ->
 	  VernacPrint (PrintModuleType qid)
       | IDENT "Print"; IDENT "Module"; qid = global ->
@@ -940,8 +940,8 @@ GEXTEND Gram
       | IDENT "Check"; c = lconstr; "." ->
 	 fun g -> VernacCheckMayEval (None, g, c)
       (* Searching the environment *)
-      | IDENT "About"; qid = smart_global; "." ->
-	 fun g -> VernacPrint (PrintAbout (qid,g))
+      | IDENT "About"; qid = smart_global; l = OPT univ_name_list; "." ->
+         fun g -> VernacPrint (PrintAbout (qid,l,g))
       | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules; "." ->
 	  fun g -> VernacSearch (SearchHead c,g, l)
       | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules; "." ->
@@ -960,7 +960,7 @@ GEXTEND Gram
       ] ]
   ;
   printable:
-    [ [ IDENT "Term"; qid = smart_global -> PrintName qid
+    [ [ IDENT "Term"; qid = smart_global; l = OPT univ_name_list -> PrintName (qid,l)
       | IDENT "All" -> PrintFullContext
       | IDENT "Section"; s = global -> PrintSectionContext s
       | IDENT "Grammar"; ent = IDENT ->
@@ -1060,6 +1060,9 @@ GEXTEND Gram
       | -> ([],SearchOutside [])
       ] ]
   ;
+  univ_name_list:
+    [ [  "@{" ; l = LIST0 name; "}" -> l ] ]
+  ;
 END;
 
 GEXTEND Gram
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index e897b1938..1a74538aa 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -41,6 +41,11 @@ open Decl_kinds
     pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
       pr_glob_level r
 
+  let pr_univ_name_list = function
+    | None -> mt ()
+    | Some l ->
+      str "@{" ++ prlist_with_sep spc pr_lname l ++ str"}"
+
   let pr_univdecl_instance l extensible =
     prlist_with_sep spc pr_lident l ++
     (if extensible then str"+" else mt ())
@@ -488,8 +493,8 @@ open Decl_kinds
         else "Print Universes"
       in
       keyword cmd ++ pr_opt str fopt
-    | PrintName qid ->
-      keyword "Print" ++ spc()  ++ pr_smart_global qid
+    | PrintName (qid,udecl) ->
+      keyword "Print" ++ spc()  ++ pr_smart_global qid ++ pr_univ_name_list udecl
     | PrintModuleType qid ->
       keyword "Print Module Type" ++ spc() ++ pr_reference qid
     | PrintModule qid ->
@@ -502,9 +507,9 @@ open Decl_kinds
       keyword "Print Scope" ++ spc() ++ str s
     | PrintVisibility s ->
       keyword "Print Visibility" ++ pr_opt str s
-    | PrintAbout (qid,gopt) ->
+    | PrintAbout (qid,l,gopt) ->
        pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt
-       ++ keyword "About" ++ spc()  ++ pr_smart_global qid
+       ++ keyword "About" ++ spc()  ++ pr_smart_global qid ++ pr_univ_name_list l
     | PrintImplicit qid ->
       keyword "Print Implicit" ++ spc()  ++ pr_smart_global qid
     (* spiwack: command printing all the axioms and section variables used in a
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index b4ac94103..602b7a496 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -32,8 +32,8 @@ open Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
 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;
@@ -68,7 +68,7 @@ let int_or_no n = if Int.equal n 0 then str "no" else int n
 
 let print_basename sp = pr_global (ConstRef sp)
 
-let print_ref reduce ref =
+let print_ref reduce ref udecl =
   let typ, ctx = Global.type_of_global_in_context (Global.env ()) ref in
   let typ = Vars.subst_instance_constr (Univ.AUContext.instance ctx) typ in
   let typ = EConstr.of_constr typ in
@@ -81,7 +81,8 @@ let print_ref reduce ref =
   let inst = Univ.AUContext.instance univs in
   let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
   let env = Global.env () in
-  let bl = Universes.universe_binders_of_global ref in
+  let bl = Universes.universe_binders_with_opt_names ref
+      (Array.to_list (Univ.Instance.to_array inst)) udecl in
   let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
   let inst =
     if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs
@@ -150,7 +151,7 @@ let print_impargs ref =
   let has_impl = not (List.is_empty impl) in
   (* Need to reduce since implicits are computed with products flattened *)
   pr_infos_list
-    ([ print_ref (need_expansion (select_impargs_size 0 impl) ref) ref;
+    ([ print_ref (need_expansion (select_impargs_size 0 impl) ref) ref None;
        blankline ] @
     (if has_impl then print_impargs_list (mt()) impl
      else [str "No implicit arguments"]))
@@ -256,7 +257,7 @@ let print_name_infos ref =
     if need_expansion (select_impargs_size 0 impls) ref then
       (* Need to reduce since implicits are computed with products flattened *)
       [str "Expanded type for implicit arguments";
-       print_ref true ref; blankline]
+       print_ref true ref None; blankline]
     else
       [] in
   print_polymorphism ref @
@@ -512,11 +513,11 @@ let assumptions_for_print lna =
 (*********************)
 (* *)
 
-let gallina_print_inductive sp =
+let gallina_print_inductive sp udecl =
   let env = Global.env() in
   let mib = Environ.lookup_mind sp env in
   let mipv = mib.mind_packets in
-  pr_mutual_inductive_body env sp mib ++
+  pr_mutual_inductive_body env sp mib udecl ++
   with_line_skip
     (print_primitive_record mib.mind_finite mipv mib.mind_record @
      print_inductive_renames sp mipv @
@@ -545,7 +546,7 @@ let print_instance sigma cb =
     pr_universe_instance sigma univs
   else mt()
 				
-let print_constant with_values sep sp =
+let print_constant with_values sep sp udecl =
   let cb = Global.lookup_constant sp in
   let val_0 = Global.body_of_constant_body cb in
   let typ =
@@ -555,31 +556,34 @@ let print_constant with_values sep sp =
       let inst = Univ.AUContext.instance univs in
       Vars.subst_instance_constr inst cb.const_type
   in
-  let univs =
+  let univs, ulist =
     let open Entries in
+    let open Univ in
     let otab = Global.opaque_tables () in
     match cb.const_body with
     | Undef _ | Def _ ->
       begin
         match cb.const_universes with
-        | Monomorphic_const ctx -> Monomorphic_const_entry ctx
+        | Monomorphic_const ctx -> Monomorphic_const_entry ctx, []
         | Polymorphic_const ctx ->
-          let inst = Univ.AUContext.instance ctx in
-          Polymorphic_const_entry (Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx))
+          let inst = AUContext.instance ctx in
+          Polymorphic_const_entry (UContext.make (inst, AUContext.instantiate inst ctx)),
+          Array.to_list (Instance.to_array inst)
       end
     | OpaqueDef o ->
       let body_uctxs = Opaqueproof.force_constraints otab o in
       match cb.const_universes with
       | Monomorphic_const ctx ->
-        Monomorphic_const_entry (Univ.ContextSet.union body_uctxs ctx)
+        Monomorphic_const_entry (ContextSet.union body_uctxs ctx), []
       | Polymorphic_const ctx ->
-        assert(Univ.ContextSet.is_empty body_uctxs);
-        let inst = Univ.AUContext.instance ctx in
-        Polymorphic_const_entry (Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx))
+        assert(ContextSet.is_empty body_uctxs);
+        let inst = AUContext.instance ctx in
+        Polymorphic_const_entry (UContext.make (inst, AUContext.instantiate inst ctx)),
+        Array.to_list (Instance.to_array inst)
   in
   let ctx =
     Evd.evar_universe_context_of_binders
-      (Universes.universe_binders_of_global (ConstRef sp))
+      (Universes.universe_binders_with_opt_names (ConstRef sp) ulist udecl)
   in
   let env = Global.env () and sigma = Evd.from_ctx ctx in
   let pr_ltype = pr_ltype_env env sigma in
@@ -596,8 +600,8 @@ let print_constant with_values sep sp =
 	(if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++
         Printer.pr_constant_universes sigma univs)
 
-let gallina_print_constant_with_infos sp =
-  print_constant true " = " sp ++
+let gallina_print_constant_with_infos sp udecl =
+  print_constant true " = " sp udecl ++
   with_line_skip (print_name_infos (ConstRef sp))
 
 let gallina_print_syntactic_def env kn =
@@ -622,9 +626,9 @@ let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) =
              constraints *)
           (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None)
       | (_,"CONSTANT") ->
-	  Some (print_constant with_values sep (Constant.make1 kn))
+          Some (print_constant with_values sep (Constant.make1 kn) None)
       | (_,"INDUCTIVE") ->
-	  Some (gallina_print_inductive (MutInd.make1 kn))
+          Some (gallina_print_inductive (MutInd.make1 kn) None)
       | (_,"MODULE") ->
 	  let (mp,_,l) = KerName.repr kn in
 	    Some (print_module with_values (MPdot (mp,l)))
@@ -745,7 +749,7 @@ let print_full_pure_context env sigma =
       | "INDUCTIVE" ->
 	  let mind = Global.mind_of_delta_kn kn in
 	  let mib = Global.lookup_mind mind in
-	  pr_mutual_inductive_body (Global.env()) mind mib ++
+          pr_mutual_inductive_body (Global.env()) mind mib None ++
 	    str "." ++ fnl () ++ fnl ()
       | "MODULE" ->
 	  (* TODO: make it reparsable *)
@@ -792,10 +796,19 @@ let print_sec_context env sigma sec =
 let print_sec_context_typ env sigma sec =
   print_context env sigma false None (read_sec_context sec)
 
-let print_any_name env sigma = function
-  | Term (ConstRef sp) -> print_constant_with_infos sp
-  | Term (IndRef (sp,_)) -> print_inductive sp
-  | Term (ConstructRef ((sp,_),_)) -> print_inductive sp
+let maybe_error_reject_univ_decl na udecl =
+  match na, udecl with
+  | _, None | Term (ConstRef _ | IndRef _ | ConstructRef _), Some _ -> ()
+  | (Term (VarRef _) | Syntactic _ | Dir _ | ModuleType _ | Other _ | Undefined _), Some udecl ->
+    (* TODO Print na somehow *)
+    user_err ~hdr:"reject_univ_decl" (str "This object does not support universe names.")
+
+let print_any_name env sigma na udecl =
+  maybe_error_reject_univ_decl na udecl;
+  match na with
+  | Term (ConstRef sp) -> print_constant_with_infos sp udecl
+  | Term (IndRef (sp,_)) -> print_inductive sp udecl
+  | Term (ConstructRef ((sp,_),_)) -> print_inductive sp udecl
   | Term (VarRef sp) -> print_section_variable env sigma sp
   | Syntactic kn -> print_syntactic_def env kn
   | Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp
@@ -812,24 +825,26 @@ let print_any_name env sigma = function
     user_err
       ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
 
-let print_name env sigma = function
+let print_name env sigma na udecl =
+  match na with
   | ByNotation (loc,(ntn,sc)) ->
       print_any_name env sigma
         (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
                ntn sc))
+        udecl
   | AN ref ->
-      print_any_name env sigma (locate_any_name ref)
+      print_any_name env sigma (locate_any_name ref) udecl
 
 let print_opaque_name env sigma qid =
   match Nametab.global qid with
     | ConstRef cst ->
 	let cb = Global.lookup_constant cst in
         if Declareops.constant_has_body cb then
-	  print_constant_with_infos cst
+          print_constant_with_infos cst None
         else
 	  user_err Pp.(str "Not a defined constant.")
     | IndRef (sp,_) ->
-        print_inductive sp
+        print_inductive sp None
     | ConstructRef cstr as gr ->
 	let ty, ctx = Global.type_of_global_in_context env gr in
 	let inst = Univ.AUContext.instance ctx in
@@ -840,13 +855,14 @@ let print_opaque_name env sigma qid =
     | VarRef id ->
         env |> lookup_named id |> print_named_decl env sigma
 
-let print_about_any ?loc env sigma k =
+let print_about_any ?loc env sigma k udecl =
+  maybe_error_reject_univ_decl k udecl;
   match k with
   | Term ref ->
     let rb = Reductionops.ReductionBehaviour.print ref in
     Dumpglob.add_glob ?loc ref;
       pr_infos_list
-       (print_ref false ref :: blankline ::
+       (print_ref false ref udecl :: blankline ::
 	print_name_infos ref @
 	(if Pp.ismt rb then [] else [rb]) @
 	print_opacity ref @
@@ -862,13 +878,14 @@ let print_about_any ?loc env sigma k =
       hov 0 (pr_located_qualid k)
   | Other (obj, info) -> hov 0 (info.about obj)
 
-let print_about env sigma = function
+let print_about env sigma na udecl =
+  match na with
   | ByNotation (loc,(ntn,sc)) ->
       print_about_any ?loc env sigma
         (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
-               ntn sc))
+               ntn sc)) udecl
   | AN ref ->
-      print_about_any ?loc:(loc_of_reference ref) env sigma (locate_any_name ref)
+      print_about_any ?loc:(loc_of_reference ref) env sigma (locate_any_name ref) udecl
 
 (* for debug *)
 let inspect env sigma depth =
@@ -940,7 +957,7 @@ let print_canonical_projections env sigma =
 open Typeclasses
 
 let pr_typeclass env t =
-  print_ref false t.cl_impl
+  print_ref false t.cl_impl None
 
 let print_typeclasses () =
   let env = Global.env () in
@@ -949,7 +966,7 @@ let print_typeclasses () =
 let pr_instance env i =
   (*   gallina_print_constant_with_infos i.is_impl *)
   (* lighter *)
-  print_ref false (instance_impl i) ++
+  print_ref false (instance_impl i) None ++
   begin match hint_priority i with
   | None -> mt ()
   | Some i -> spc () ++ str "|" ++ spc () ++ int i
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 89099a043..8f3a6ddc4 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;
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 13a03e9b4..c34543bbd 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -121,7 +121,7 @@ let instantiate_cumulativity_info cumi =
   in
   CumulativityInfo.make (expose univs, expose subtyp)
 
-let print_mutual_inductive env mind mib =
+let print_mutual_inductive env mind mib udecl =
   let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
   in
   let keyword =
@@ -131,7 +131,14 @@ let print_mutual_inductive env mind mib =
     | BiFinite -> "Variant"
     | CoFinite -> "CoInductive"
   in
-  let bl = Universes.universe_binders_of_global (IndRef (mind, 0)) in
+  let univs =
+    let open Univ in
+    if Declareops.inductive_is_polymorphic mib then
+      Array.to_list (Instance.to_array
+                       (AUContext.instance (Declareops.inductive_polymorphic_context mib)))
+    else []
+  in
+  let bl = Universes.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in
   let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
   hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
          Printer.pr_cumulative
@@ -159,7 +166,7 @@ let get_fields =
   in
   prodec_rec [] []
 
-let print_record env mind mib =
+let print_record env mind mib udecl =
   let u = 
     if Declareops.inductive_is_polymorphic mib then 
       Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib)
@@ -173,7 +180,8 @@ let print_record env mind mib =
   let cstrtype = hnf_prod_applist env cstrtypes.(0) args in
   let fields = get_fields cstrtype in
   let envpar = push_rel_context params env in
-  let bl = Universes.universe_binders_of_global (IndRef (mind,0)) in
+  let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0))
+      (Array.to_list (Univ.Instance.to_array u)) udecl in
   let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
   let keyword =
     let open Decl_kinds in
@@ -205,11 +213,11 @@ let print_record env mind mib =
         sigma (instantiate_cumulativity_info cumi)
   )
 
-let pr_mutual_inductive_body env mind mib =
+let pr_mutual_inductive_body env mind mib udecl =
   if mib.mind_record <> None && not !Flags.raw_print then
-    print_record env mind mib
+    print_record env mind mib udecl
   else
-    print_mutual_inductive env mind mib
+    print_mutual_inductive env mind mib udecl
 
 (** Modpaths *)
 
@@ -335,7 +343,7 @@ let print_body is_impl env mp (l,body) =
     | SFBmind mib ->
       try
 	let env = Option.get env in
-	pr_mutual_inductive_body env (MutInd.make2 mp l) mib
+        pr_mutual_inductive_body env (MutInd.make2 mp l) mib None
       with e when CErrors.noncritical e ->
         let keyword =
           let open Decl_kinds in
diff --git a/printing/printmod.mli b/printing/printmod.mli
index b0bbb21e0..97ed063fe 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -11,6 +11,8 @@ open Names
 (** false iff the module is an element of an open module type *)
 val printable_body : DirPath.t -> bool
 
-val pr_mutual_inductive_body : Environ.env -> MutInd.t -> Declarations.mutual_inductive_body -> Pp.t
+val pr_mutual_inductive_body : Environ.env ->
+  MutInd.t -> Declarations.mutual_inductive_body ->
+  Vernacexpr.univ_name_list option -> Pp.t
 val print_module : bool -> ModPath.t -> Pp.t
 val print_modtype : ModPath.t -> Pp.t
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 42fb52a3b..6fb8cba18 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -53,3 +53,34 @@ Monomorphic mono = Type@{u}
 (* {u} |=  *)
 
 mono is not universe polymorphic
+foo@{E M N} = 
+Type@{M} -> Type@{N} -> Type@{E}
+     : Type@{max(E+1, M+1, N+1)}
+(* E M N |=  *)
+
+foo is universe polymorphic
+foo@{Top.16 Top.17 Top.18} = 
+Type@{Top.17} -> Type@{Top.18} -> Type@{Top.16}
+     : Type@{max(Top.16+1, Top.17+1, Top.18+1)}
+(* Top.16 Top.17 Top.18 |=  *)
+
+foo is universe polymorphic
+NonCumulative Inductive Empty@{E} : Type@{E} :=  
+NonCumulative Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
+
+PWrap has primitive projections with eta conversion.
+For PWrap: Argument scope is [type_scope]
+For pwrap: Argument scopes are [type_scope _]
+punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A
+(* K |=  *)
+
+punwrap is universe polymorphic
+Argument scopes are [type_scope _]
+punwrap is transparent
+Expands to: Constant Top.punwrap
+The command has indeed failed with message:
+Universe instance should have length 3
+The command has indeed failed with message:
+Universe instance should have length 0
+The command has indeed failed with message:
+This object does not support universe names.
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 2c378e795..46904b384 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -33,3 +33,22 @@ Print foo.
 (* Binders even work with monomorphic definitions! *)
 Monomorphic Definition mono@{u} := Type@{u}.
 Print mono.
+
+(* Using local binders for printing. *)
+Print foo@{E M N}.
+(* Underscores discard the name if there's one. *)
+Print foo@{_ _ _}.
+
+(* Also works for inductives and records. *)
+Print Empty@{E}.
+Print PWrap@{E}.
+
+(* Also works for About. *)
+About punwrap@{K}.
+
+(* Instance length check. *)
+Fail Print foo@{E}.
+Fail Print mono@{E}.
+
+(* Not everything can be printed with custom universe names. *)
+Fail Print Coq.Init.Logic@{E}.
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e2f28a371..22e3e9c99 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1609,9 +1609,10 @@ exception NoHyp
 (* Printing "About" information of a hypothesis of the current goal.
    We only print the type and a small statement to this comes from the
    goal. Precondition: there must be at least one current goal. *)
-let print_about_hyp_globs ?loc ref_or_by_not glopt =
+let print_about_hyp_globs ?loc ref_or_by_not udecl glopt =
   let open Context.Named.Declaration in
   try
+    (* FIXME error on non None udecl if we find the hyp. *)
     let glnumopt = query_command_selector ?loc glopt in
     let gl,id =
       match glnumopt,ref_or_by_not with
@@ -1634,7 +1635,7 @@ let print_about_hyp_globs ?loc ref_or_by_not glopt =
   with (* fallback to globals *)
     | NoHyp | Not_found ->
     let sigma, env = Pfedit.get_current_context () in
-    print_about env sigma ref_or_by_not
+    print_about env sigma ref_or_by_not udecl
 
 
 let vernac_print ?loc env sigma = let open Feedback in function
@@ -1651,7 +1652,7 @@ let vernac_print ?loc env sigma = let open Feedback in function
   | PrintMLLoadPath -> msg_notice (Mltop.print_ml_path ())
   | PrintMLModules -> msg_notice (Mltop.print_ml_modules ())
   | PrintDebugGC -> msg_notice (Mltop.print_gc ())
-  | PrintName qid -> dump_global qid; msg_notice (print_name env sigma qid)
+  | PrintName (qid,udecl) -> dump_global qid; msg_notice (print_name env sigma qid udecl)
   | PrintGraph -> msg_notice (Prettyp.print_graph())
   | PrintClasses -> msg_notice (Prettyp.print_classes())
   | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses())
@@ -1681,8 +1682,8 @@ let vernac_print ?loc env sigma = let open Feedback in function
       msg_notice (Notation.pr_scope (Constrextern.without_symbols (pr_lglob_constr_env env)) s)
   | PrintVisibility s ->
       msg_notice (Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s)
-  | PrintAbout (ref_or_by_not,glnumopt) ->
-     msg_notice (print_about_hyp_globs ?loc ref_or_by_not glnumopt)
+  | PrintAbout (ref_or_by_not,udecl,glnumopt) ->
+     msg_notice (print_about_hyp_globs ?loc ref_or_by_not udecl glnumopt)
   | PrintImplicit qid ->
     dump_global qid; msg_notice (print_impargs qid)
   | PrintAssumptions (o,t,r) ->