Search: Displaying the "use About" notice only when really needed.

6 files changed, 13 insertions, 44 deletions

diff --git a/clib/cList.mli b/clib/cList.mli
index 07f42770f9..c8e471f989 100644
--- a/clib/cList.mli
+++ b/clib/cList.mli
@@ -265,7 +265,7 @@ sig
       This is the second part of [chop]. *)
 
   val skipn_at_least : int -> 'a list -> 'a list
-  (** Same as [skipn] but returns [] if [n] is larger than the list of
+  (** Same as [skipn] but returns [] if [n] is larger than the length of
       the list. *)
 
   val drop_prefix : 'a eq -> 'a list -> 'a list -> 'a list
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index c01f4b2e19..a527b5e9f8 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -18,7 +18,6 @@ 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
 is_true: bool -> Prop
@@ -136,7 +135,6 @@ bool_choice:
   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
@@ -162,7 +160,6 @@ 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)
 Numeral.internal_numeral_dec_lb:
   forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true
 Numeral.internal_int_dec_lb1:
@@ -216,7 +213,6 @@ bool_choice:
   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)
 Numeral.internal_numeral_dec_lb:
   forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true
 Numeral.internal_numeral_dec_bl:
@@ -266,23 +262,15 @@ Hexadecimal.internal_uint_dec_lb0:
 andb_true_intro:
   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:
 [Focus] No such goal.
 The command has indeed failed with message:
@@ -291,14 +279,9 @@ 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 d42dc575c2..61ceab72f8 100644
--- a/test-suite/output/SearchHead.out
+++ b/test-suite/output/SearchHead.out
@@ -4,7 +4,6 @@ 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
@@ -28,7 +27,6 @@ Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool
 Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool
 Decimal.int_beq: Decimal.int -> Decimal.int -> bool
 Decimal.uint_beq: Decimal.uint -> Decimal.uint -> 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
@@ -47,8 +45,5 @@ 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 13d0a9e55b..80b03e8a0b 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -21,7 +21,6 @@ Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool
 Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool
 Decimal.int_beq: Decimal.int -> Decimal.int -> bool
 Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool
-(use "About" for full details on implicit arguments)
 Nat.two: nat
 Nat.zero: nat
 Nat.one: nat
@@ -61,8 +60,6 @@ Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
 Nat.log2_iter: nat -> nat -> nat -> nat -> 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
@@ -92,29 +89,19 @@ Nat.of_hex_uint_acc: Hexadecimal.uint -> nat -> nat
 Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
 Nat.log2_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
 Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
-(use "About" for full details on implicit arguments)
+(use "About" for full details on the implicit arguments of eq_refl)
 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 3c0880b20c..5edea5dff6 100644
--- a/test-suite/output/SearchRewrite.out
+++ b/test-suite/output/SearchRewrite.out
@@ -1,10 +1,5 @@
 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/vernacentries.ml b/vernac/vernacentries.ml
index 75873381bf..c7e8d9a3b9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1852,14 +1852,20 @@ let vernac_search ~pstate ~atts s gopt r =
     | Some g -> snd (get_goal_or_global_context ~pstate g) , Some g
   in
   let get_pattern c = snd (Constrintern.intern_constr_pattern env Evd.(from_env env) c) in
+  let warnlist = ref [] in
   let pr_search ref kind env c =
     let pr = pr_global ref in
     let pp = if !search_output_name_only
       then pr
       else begin
         let open Impargs in
-        let impargs = select_stronger_impargs (implicits_of_global ref) in
+        let impls = implicits_of_global ref in
+        let impargs = select_stronger_impargs impls in
         let impargs = List.map binding_kind_of_status impargs in
+        if List.length impls > 1 ||
+           List.exists Glob_term.(function Explicit -> false | MaxImplicit | NonMaxImplicit -> true)
+             (List.skipn_at_least (Termops.nb_prod_modulo_zeta Evd.(from_env env) (EConstr.of_constr c)) impargs)
+          then warnlist := pr :: !warnlist;
         let pc = pr_ltype_env env Evd.(from_env env) ~impargs c in
         hov 2 (pr ++ str":" ++ spc () ++ pc)
       end
@@ -1875,7 +1881,10 @@ let vernac_search ~pstate ~atts s gopt r =
   | Search sl ->
       (Search.search ?pstate gopt (List.map (interp_search_request env Evd.(from_env env)) sl) r |>
        Search.prioritize_search) pr_search);
-  Feedback.msg_notice (str "(use \"About\" for full details on implicit arguments)")
+  if !warnlist <> [] then
+  Feedback.msg_notice (str "(" ++
+    hov 0 (strbrk "use \"About\" for full details on the implicit arguments of " ++
+           pr_enum (fun x -> x) !warnlist ++ str ")"))
 
 let vernac_locate ~pstate = let open Constrexpr in function
   | LocateAny {v=AN qid}  -> Prettyp.print_located_qualid qid