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

4 files changed, 1 insertions, 41 deletions

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)