Merge PR #11795: Print implicit arguments in types of references

Ack-by: herbelin

17 files changed, 117 insertions, 55 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index ebe704b88a..96dbf9142b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -82,7 +82,7 @@ let ppsconstr x = ppconstr (Mod_subst.force_constr x)
 let ppconstr_univ x = Constrextern.with_universes ppconstr x
 let ppglob_constr = (fun x -> pp(pr_lglob_constr_env (Global.env()) x))
 let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x))
-let pptype = (fun x -> try pp(envpp pr_ltype_env x) with e -> pp (str (Printexc.to_string e)))
+let pptype = (fun x -> try pp(envpp (fun env evm t -> pr_ltype_env env evm t) x) with e -> pp (str (Printexc.to_string e)))
 let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
 
 let ppbigint n = pp (str (Bigint.to_string n));;
diff --git a/doc/changelog/07-commands-and-options/11795-print_implicit_args.rst b/doc/changelog/07-commands-and-options/11795-print_implicit_args.rst
new file mode 100644
index 0000000000..5b0cdb5914
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11795-print_implicit_args.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  Several commands (`Search`, `About`, ...) now print the implicit arguments
+  in brackets when printing types.
+  (`#11795 <https://github.com/coq/coq/pull/11795>`_,
+  by SimonBoulier).
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 631408c032..a16825b5c9 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -926,7 +926,7 @@ let extern_ref vars ref us =
 
 let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None)
 
-let rec extern inctx scopes vars r =
+let rec extern inctx ?impargs scopes vars r =
   match remove_one_coercion inctx (flatten_application r) with
   | Some (nargs,inctx,r') ->
     (try extern_notations scopes vars (Some nargs) r
@@ -990,10 +990,10 @@ let rec extern inctx scopes vars r =
   | GLetIn (na,b,t,c) ->
       CLetIn (make ?loc na,sub_extern false scopes vars b,
               Option.map (extern_typ scopes vars) t,
-              extern inctx scopes (add_vname vars na) c)
+              extern inctx ?impargs scopes (add_vname vars na) c)
 
   | GProd (na,bk,t,c) ->
-      factorize_prod scopes vars na bk t c
+      factorize_prod ?impargs scopes vars na bk t c
 
   | GLambda (na,bk,t,c) ->
       factorize_lambda inctx scopes vars na bk t c
@@ -1092,12 +1092,12 @@ let rec extern inctx scopes vars r =
 
   in insert_coercion coercion (CAst.make ?loc c)
 
-and extern_typ (subentry,(_,scopes)) =
-  extern true (subentry,(Notation.current_type_scope_name (),scopes))
+and extern_typ ?impargs (subentry,(_,scopes)) =
+  extern true ?impargs (subentry,(Notation.current_type_scope_name (),scopes))
 
 and sub_extern inctx (subentry,(_,scopes)) = extern inctx (subentry,(None,scopes))
 
-and factorize_prod scopes vars na bk t c =
+and factorize_prod ?impargs scopes vars na bk t c =
   let implicit_type = is_reserved_type na t in
   let aty = extern_typ scopes vars t in
   let vars = add_vname vars na in
@@ -1117,7 +1117,13 @@ and factorize_prod scopes vars na bk t c =
       | _ -> CProdN ([binder],b))
      | _ -> assert false)
   | _, _ ->
-      let c' = extern_typ scopes vars c in
+      let impargs_hd, impargs_tl =
+        match impargs with
+        | Some [hd] -> Some hd, None
+        | Some (hd::tl) -> Some hd, Some tl
+        | _ -> None, None in
+      let bk = Option.default Explicit impargs_hd in
+      let c' = extern_typ ?impargs:impargs_tl scopes vars c in
       match na, c'.v with
       | Name id, CProdN (CLocalAssum(nal,Default bk',ty)::bl,b)
            when binding_kind_eq bk bk'
@@ -1306,8 +1312,8 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
 let extern_glob_constr vars c =
   extern false (InConstrEntrySomeLevel,(None,[])) vars c
 
-let extern_glob_type vars c =
-  extern_typ (InConstrEntrySomeLevel,(None,[])) vars c
+let extern_glob_type ?impargs vars c =
+  extern_typ ?impargs (InConstrEntrySomeLevel,(None,[])) vars c
 
 (******************************************************************)
 (* Main translation function from constr -> constr_expr *)
@@ -1320,7 +1326,7 @@ let extern_constr ?lax ?(inctx=false) ?scope env sigma t =
 let extern_constr_in_scope ?lax ?inctx scope env sigma t =
   extern_constr ?lax ?inctx ~scope env sigma t
 
-let extern_type ?lax ?(goal_concl_style=false) env sigma t =
+let extern_type ?lax ?(goal_concl_style=false) env sigma ?impargs t =
   (* "goal_concl_style" means do alpha-conversion using the "goal" convention *)
   (* i.e.: avoid using the names of goal/section/rel variables and the short *)
   (* names of global definitions of current module when computing names for *)
@@ -1330,7 +1336,7 @@ let extern_type ?lax ?(goal_concl_style=false) env sigma t =
   (* consideration; see namegen.ml for further details *)
   let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
   let r = Detyping.detype Detyping.Later ?lax goal_concl_style avoid env sigma t in
-  extern_glob_type (vars_of_env env) r
+  extern_glob_type ?impargs (vars_of_env env) r
 
 let extern_sort sigma s = extern_glob_sort (detype_sort sigma s)
 
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index fe64661a66..f85e49d2df 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -25,7 +25,7 @@ open Ltac_pretype
 
 val extern_cases_pattern : Id.Set.t -> 'a cases_pattern_g -> cases_pattern_expr
 val extern_glob_constr : Id.Set.t -> 'a glob_constr_g -> constr_expr
-val extern_glob_type : Id.Set.t -> 'a glob_constr_g -> constr_expr
+val extern_glob_type : ?impargs:Glob_term.binding_kind list -> Id.Set.t -> 'a glob_constr_g -> constr_expr
 val extern_constr_pattern : names_context -> Evd.evar_map ->
   constr_pattern -> constr_expr
 val extern_closed_glob : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name ->
@@ -42,7 +42,7 @@ val extern_constr : ?lax:bool -> ?inctx:bool -> ?scope:scope_name ->
 val extern_constr_in_scope : ?lax:bool -> ?inctx:bool -> scope_name ->
   env -> Evd.evar_map -> constr -> constr_expr
 val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
-val extern_type : ?lax:bool -> ?goal_concl_style:bool -> env -> Evd.evar_map -> types -> constr_expr
+val extern_type : ?lax:bool -> ?goal_concl_style:bool -> env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> types -> constr_expr
 val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort
 val extern_rel_context : constr option -> env -> Evd.evar_map ->
   rel_context -> local_binder_expr list
diff --git a/printing/printer.ml b/printing/printer.ml
index 70fdd43908..32dc4bb0f0 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -106,8 +106,8 @@ let pr_letype_env = Proof_diffs.pr_letype_env
 
 let pr_type_env ?lax ?goal_concl_style env sigma c =
   pr_etype_env ?lax ?goal_concl_style env sigma (EConstr.of_constr c)
-let pr_ltype_env ?lax ?goal_concl_style env sigma c =
-  pr_letype_env ?lax ?goal_concl_style env sigma (EConstr.of_constr c)
+let pr_ltype_env ?lax ?goal_concl_style env sigma ?impargs c =
+  pr_letype_env ?lax ?goal_concl_style env sigma ?impargs (EConstr.of_constr c)
 
 let pr_ljudge_env env sigma j =
   (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type)
diff --git a/printing/printer.mli b/printing/printer.mli
index 8b8157fba4..936426949c 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -45,6 +45,10 @@ val enable_goal_names_printing     : bool ref
     intended to be printed in scope [some_scope_name]. It defaults to
     [None].
 
+    [~impargs:some_list_of_binding_kind] indicates the implicit arguments
+    of the external quatification. Only used for printing types (not
+    terms), and at toplevel (only "l" versions). It defaults to [None].
+
     [~lax:true] is for debugging purpose. It defaults to [~lax:false]. *)
 
 
@@ -66,7 +70,7 @@ val pr_leconstr_env     : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -
 val pr_econstr_n_env    : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> EConstr.t -> Pp.t
 
 val pr_etype_env        : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t
-val pr_letype_env       : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t
+val pr_letype_env       : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> ?impargs:Glob_term.binding_kind list -> EConstr.types -> Pp.t
 
 val pr_open_constr_env  : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> open_constr -> Pp.t
 val pr_open_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> open_constr -> Pp.t
@@ -97,7 +101,7 @@ val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp
 
     [~lax:true] is for debugging purpose. *)
 
-val pr_ltype_env           : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t
+val pr_ltype_env           : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> ?impargs:Glob_term.binding_kind list -> types -> Pp.t
 val pr_type_env            : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t
 
 val pr_closed_glob_n_env   : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> closed_glob_constr -> Pp.t
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index da76bc130d..fb91ea7b5c 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -244,9 +244,9 @@ let process_goal sigma g : EConstr.t reified_goal =
   let hyps      = List.map to_tuple hyps in
   { name; ty; hyps; env; sigma };;
 
-let pr_letype_env ?lax ?goal_concl_style env sigma t =
+let pr_letype_env ?lax ?goal_concl_style env sigma ?impargs t =
   Ppconstr.pr_lconstr_expr env sigma
-    (Constrextern.extern_type ?lax ?goal_concl_style env sigma t)
+    (Constrextern.extern_type ?lax ?goal_concl_style env sigma ?impargs t)
 
 let pp_of_type env sigma ty =
   pr_letype_env ~goal_concl_style:true env sigma ty
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index 59b7beb794..83e721d3d5 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -57,7 +57,7 @@ val diff_goal : ?og_s:(Goal.goal sigma) -> Goal.goal -> Evd.evar_map -> Pp.t
 (** Convert a string to a list of token strings using the lexer *)
 val tokenize_string : string -> string list
 
-val pr_letype_env          : ?lax:bool -> ?goal_concl_style:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t
+val pr_letype_env          : ?lax:bool -> ?goal_concl_style:bool -> Environ.env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> EConstr.types -> Pp.t
 val pr_leconstr_env        : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
 val pr_lconstr_env         : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> env -> evar_map -> constr -> Pp.t
 
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index f889da4e98..8cf0797b17 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -39,7 +39,7 @@ The reduction tactics unfold Nat.sub when the 1st and
 Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 pf :
-forall D1 C1 : Type,
+forall {D1 C1 : Type},
 (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2
 
 pf is not universe polymorphic
@@ -47,7 +47,7 @@ Arguments pf {D1}%foo_scope {C1}%type_scope _ [D2 C2] : simpl never
 The reduction tactics never unfold pf
 pf is transparent
 Expands to: Constant Arguments.pf
-fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
+fcomp : forall {A B C : Type}, (B -> C) -> (A -> B) -> A -> C
 
 fcomp is not universe polymorphic
 Arguments fcomp {A B C}%type_scope _ _ _ /
@@ -75,7 +75,7 @@ The reduction tactics unfold f when the 3rd, 4th and
   5th arguments evaluate to a constructor
 f is transparent
 Expands to: Constant Arguments.S1.S2.f
-f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
+f : forall [T2 : Type], T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
 Arguments f [T2]%type_scope _ _ !_%nat_scope !_ !_%nat_scope
@@ -83,7 +83,7 @@ The reduction tactics unfold f when the 4th, 5th and
   6th arguments evaluate to a constructor
 f is transparent
 Expands to: Constant Arguments.S1.f
-f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
+f : forall [T1 T2 : Type], T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
 Arguments f [T1 T2]%type_scope _ _ !_%nat_scope !_ !_%nat_scope
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 26ebd8efc3..abc7f0f88e 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -15,7 +15,7 @@ Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
 Arguments eq {A}%type_scope
 Arguments eq_refl {B}%type_scope {y}, [B] _
-eq_refl : forall (A : Type) (x : A), x = x
+eq_refl : forall {A : Type} {x : A}, x = x
 
 eq_refl is not universe polymorphic
 Arguments eq_refl {B}%type_scope {y}, [B] _
@@ -24,7 +24,7 @@ Inductive myEq (B : Type) (x : A) : A -> Prop :=  myrefl : B -> myEq B x x
 
 Arguments myEq _%type_scope
 Arguments myrefl {C}%type_scope x : rename
-myrefl : forall (B : Type) (x : A), B -> myEq B x x
+myrefl : forall {B : Type} (x : A), B -> myEq B x x
 
 myrefl is not universe polymorphic
 Arguments myrefl {C}%type_scope x : rename
@@ -38,7 +38,7 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
      : forall T : Type, T -> nat -> nat -> nat
 
 Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
-myplus : forall T : Type, T -> nat -> nat -> nat
+myplus : forall {T : Type}, T -> nat -> nat -> nat
 
 myplus is not universe polymorphic
 Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
@@ -53,7 +53,7 @@ Inductive myEq (A B : Type) (x : A) : A -> Prop :=
 
 Arguments myEq (_ _)%type_scope
 Arguments myrefl A%type_scope {C}%type_scope x : rename
-myrefl : forall (A B : Type) (x : A), B -> myEq A B x x
+myrefl : forall (A : Type) {B : Type} (x : A), B -> myEq A B x x
 
 myrefl is not universe polymorphic
 Arguments myrefl A%type_scope {C}%type_scope x : rename
@@ -69,7 +69,7 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
      : forall T : Type, T -> nat -> nat -> nat
 
 Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
-myplus : forall T : Type, T -> nat -> nat -> nat
+myplus : forall {T : Type}, T -> nat -> nat -> nat
 
 myplus is not universe polymorphic
 Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index 71d162c314..8fb267e343 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -1,4 +1,4 @@
-existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
+existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x}
 
 existT is template universe polymorphic on sigT.u0 sigT.u1
 Arguments existT [A]%type_scope _%function_scope
@@ -8,19 +8,19 @@ Inductive sigT (A : Type) (P : A -> Type) : Type :=
 
 Arguments sigT [A]%type_scope _%type_scope
 Arguments existT [A]%type_scope _%function_scope
-existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
+existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x}
 
 Argument A is implicit
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
 Arguments eq {A}%type_scope
 Arguments eq_refl {A}%type_scope {x}, [A] _
-eq_refl : forall (A : Type) (x : A), x = x
+eq_refl : forall {A : Type} {x : A}, x = x
 
 eq_refl is not universe polymorphic
 Arguments eq_refl {A}%type_scope {x}, [A] _
 Expands to: Constructor Coq.Init.Logic.eq_refl
-eq_refl : forall (A : Type) (x : A), x = x
+eq_refl : forall {A : Type} {x : A}, x = x
 
 When applied to no arguments:
   Arguments A, x are implicit and maximally inserted
@@ -65,14 +65,14 @@ bar : foo
 
 bar is not universe polymorphic
 Expanded type for implicit arguments
-bar : forall x : nat, x = 0
+bar : forall {x : nat}, x = 0
 
 Arguments bar {x}
 Expands to: Constant PrintInfos.bar
 *** [ bar : foo ]
 
 Expanded type for implicit arguments
-bar : forall x : nat, x = 0
+bar : forall {x : nat}, x = 0
 
 Arguments bar {x}
 Module Coq.Init.Peano
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index ffba1d35cc..9d8e830d64 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -18,6 +18,7 @@ le_sind:
   P n ->
   (forall m : nat, n <= m -> P m -> P (S m)) ->
   forall n0 : nat, n <= n0 -> P n0
+(use "About" for full details on implicit arguments)
 false: bool
 true: bool
 eq_true: bool -> Prop
@@ -37,7 +38,7 @@ Nat.leb: nat -> nat -> bool
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
 bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
 eq_true_ind_r:
-  forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true
+  forall (P : bool -> Prop) [b : bool], P b -> eq_true b -> P true
 eq_true_rec:
   forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b
 bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
@@ -49,9 +50,9 @@ bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
 eq_true_ind:
   forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
 eq_true_rec_r:
-  forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true
+  forall (P : bool -> Set) [b : bool], P b -> eq_true b -> P true
 eq_true_rect_r:
-  forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true
+  forall (P : bool -> Type) [b : bool], P b -> eq_true b -> P true
 bool_sind:
   forall P : bool -> SProp, P true -> P false -> forall b : bool, P b
 Byte.to_bits:
@@ -62,13 +63,13 @@ Byte.of_bits:
   Byte.byte
 andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 andb_true_intro:
-  forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
+  forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true
 BoolSpec_sind:
-  forall (P Q : Prop) (P0 : bool -> SProp),
+  forall [P Q : Prop] (P0 : bool -> SProp),
   (P -> P0 true) ->
   (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b
 BoolSpec_ind:
-  forall (P Q : Prop) (P0 : bool -> Prop),
+  forall [P Q : Prop] (P0 : bool -> Prop),
   (P -> P0 true) ->
   (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b
 Byte.to_bits_of_bits:
@@ -76,9 +77,10 @@ Byte.to_bits_of_bits:
     b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))),
   Byte.to_bits (Byte.of_bits b) = b
 bool_choice:
-  forall (S : Set) (R1 R2 : S -> Prop),
+  forall [S : Set] [R1 R2 : S -> Prop],
   (forall x : S, {R1 x} + {R2 x}) ->
   {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
+(use "About" for full details on implicit arguments)
 mult_n_O: forall n : nat, 0 = n * 0
 plus_O_n: forall n : nat, 0 + n = n
 plus_n_O: forall n : nat, n = n + 0
@@ -104,25 +106,35 @@ f_equal2_mult:
 f_equal2_nat:
   forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat),
   x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2
+(use "About" for full details on implicit arguments)
 andb_true_intro:
-  forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
+  forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true
 andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 bool_choice:
-  forall (S : Set) (R1 R2 : S -> Prop),
+  forall [S : Set] [R1 R2 : S -> Prop],
   (forall x : S, {R1 x} + {R2 x}) ->
   {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
+(use "About" for full details on implicit arguments)
 andb_true_intro:
-  forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
+  forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true
 andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
+(use "About" for full details on implicit arguments)
 andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
+(use "About" for full details on implicit arguments)
 h: n <> newdef n
 h': newdef n <> n
+(use "About" for full details on implicit arguments)
 h: n <> newdef n
 h': newdef n <> n
+(use "About" for full details on implicit arguments)
 h: n <> newdef n
+(use "About" for full details on implicit arguments)
 h: n <> newdef n
+(use "About" for full details on implicit arguments)
 h: n <> newdef n
 h': newdef n <> n
+(use "About" for full details on implicit arguments)
+(use "About" for full details on implicit arguments)
 The command has indeed failed with message:
 No such goal.
 The command has indeed failed with message:
@@ -131,9 +143,14 @@ The command has indeed failed with message:
 Query commands only support the single numbered goal selector.
 h: P n
 h': ~ P n
+(use "About" for full details on implicit arguments)
 h: P n
 h': ~ P n
+(use "About" for full details on implicit arguments)
 h: P n
 h': ~ P n
+(use "About" for full details on implicit arguments)
 h: P n
+(use "About" for full details on implicit arguments)
 h: P n
+(use "About" for full details on implicit arguments)
diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out
index 7038eac22c..5627e4bd3c 100644
--- a/test-suite/output/SearchHead.out
+++ b/test-suite/output/SearchHead.out
@@ -4,6 +4,7 @@ le_S: forall n m : nat, n <= m -> n <= S m
 le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
 le_n_S: forall n m : nat, n <= m -> S n <= S m
 le_S_n: forall n m : nat, S n <= S m -> n <= m
+(use "About" for full details on implicit arguments)
 false: bool
 true: bool
 negb: bool -> bool
@@ -17,6 +18,7 @@ Nat.leb: nat -> nat -> bool
 Nat.ltb: nat -> nat -> bool
 Nat.testbit: nat -> nat -> bool
 Nat.eqb: nat -> nat -> bool
+(use "About" for full details on implicit arguments)
 mult_n_O: forall n : nat, 0 = n * 0
 plus_O_n: forall n : nat, 0 + n = n
 plus_n_O: forall n : nat, n = n + 0
@@ -35,5 +37,8 @@ f_equal2_plus:
   forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
 f_equal2_mult:
   forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
+(use "About" for full details on implicit arguments)
 h: newdef n
+(use "About" for full details on implicit arguments)
 h: P n
+(use "About" for full details on implicit arguments)
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index 4cd0ffb1dc..36fc1a5914 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -11,6 +11,7 @@ Nat.leb: nat -> nat -> bool
 Nat.ltb: nat -> nat -> bool
 Nat.testbit: nat -> nat -> bool
 Nat.eqb: nat -> nat -> bool
+(use "About" for full details on implicit arguments)
 Nat.two: nat
 Nat.one: nat
 Nat.zero: nat
@@ -44,8 +45,10 @@ Nat.tail_addmul: nat -> nat -> nat -> nat
 Nat.of_uint_acc: Decimal.uint -> nat -> nat
 Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
 Nat.log2_iter: nat -> nat -> nat -> nat -> nat
-length: forall A : Type, list A -> nat
+length: forall [A : Type], list A -> nat
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
+(use "About" for full details on implicit arguments)
+(use "About" for full details on implicit arguments)
 Nat.div2: nat -> nat
 Nat.sqrt: nat -> nat
 Nat.log2: nat -> nat
@@ -74,18 +77,29 @@ Nat.of_uint_acc: Decimal.uint -> nat -> nat
 Nat.log2_iter: nat -> nat -> nat -> nat -> nat
 Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
+(use "About" for full details on implicit arguments)
 mult_n_Sm: forall n m : nat, n * m + n = n * S m
+(use "About" for full details on implicit arguments)
 iff_refl: forall A : Prop, A <-> A
 le_n: forall n : nat, n <= n
-identity_refl: forall (A : Type) (a : A), identity a a
-eq_refl: forall (A : Type) (x : A), x = x
+identity_refl: forall [A : Type] (a : A), identity a a
+eq_refl: forall {A : Type} {x : A}, x = x
 Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
-conj: forall A B : Prop, A -> B -> A /\ B
-pair: forall A B : Type, A -> B -> A * B
+(use "About" for full details on implicit arguments)
+conj: forall [A B : Prop], A -> B -> A /\ B
+pair: forall {A B : Type}, A -> B -> A * B
 Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
+(use "About" for full details on implicit arguments)
+(use "About" for full details on implicit arguments)
 h: n <> newdef n
+(use "About" for full details on implicit arguments)
 h: n <> newdef n
+(use "About" for full details on implicit arguments)
 h: P n
+(use "About" for full details on implicit arguments)
 h': ~ P n
+(use "About" for full details on implicit arguments)
 h: P n
+(use "About" for full details on implicit arguments)
 h: P n
+(use "About" for full details on implicit arguments)
diff --git a/test-suite/output/SearchRewrite.out b/test-suite/output/SearchRewrite.out
index 5edea5dff6..3c0880b20c 100644
--- a/test-suite/output/SearchRewrite.out
+++ b/test-suite/output/SearchRewrite.out
@@ -1,5 +1,10 @@
 plus_n_O: forall n : nat, n = n + 0
+(use "About" for full details on implicit arguments)
 plus_O_n: forall n : nat, 0 + n = n
+(use "About" for full details on implicit arguments)
 h: n = newdef n
+(use "About" for full details on implicit arguments)
 h: n = newdef n
+(use "About" for full details on implicit arguments)
 h: n = newdef n
+(use "About" for full details on implicit arguments)
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 52457d15dc..a7170c8e18 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -83,6 +83,8 @@ let print_ref reduce ref udecl =
       let ctx,ccl = Reductionops.splay_prod_assum env sigma typ
       in EConstr.it_mkProd_or_LetIn ccl ctx
     else typ in
+  let impargs = select_stronger_impargs (implicits_of_global ref) in
+  let impargs = List.map binding_kind_of_status impargs in
   let variance = let open GlobRef in match ref with
     | VarRef _ | ConstRef _ -> None
     | IndRef (ind,_) | ConstructRef ((ind,_),_) ->
@@ -95,7 +97,7 @@ let print_ref reduce ref udecl =
     else mt ()
   in
   let priv = None in (* We deliberately don't print private univs in About. *)
-  hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++
+  hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma ~impargs typ ++
          Printer.pr_abstract_universe_ctx sigma ?variance univs ?priv)
 
 (********************************)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e2fdae37fb..b5ecd62dad 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1778,12 +1778,15 @@ let vernac_search ~pstate ~atts s gopt r =
     let pp = if !search_output_name_only
       then pr
       else begin
-        let pc = pr_lconstr_env env Evd.(from_env env) c in
+        let open Impargs in
+        let impargs = select_stronger_impargs (implicits_of_global ref) in
+        let impargs = List.map binding_kind_of_status impargs in
+        let pc = pr_ltype_env env Evd.(from_env env) ~impargs c in
         hov 2 (pr ++ str":" ++ spc () ++ pc)
       end
     in Feedback.msg_notice pp
   in
-  match s with
+  (match s with
   | SearchPattern c ->
       (Search.search_pattern ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search
   | SearchRewrite c ->
@@ -1796,7 +1799,8 @@ let vernac_search ~pstate ~atts s gopt r =
        Search.prioritize_search) pr_search
   | Search sl ->
       (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |>
-       Search.prioritize_search) pr_search
+       Search.prioritize_search) pr_search);
+  Feedback.msg_notice (str "(use \"About\" for full details on implicit arguments)")
 
 let vernac_locate ~pstate = let open Constrexpr in function
   | LocateAny {v=AN qid}  -> Prettyp.print_located_qualid qid