Merge PR #8855: More search options

Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: kyoDralliam

5 files changed, 222 insertions, 41 deletions

diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index c01f4b2e19..317e9c3757 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,179 @@ 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)
+a: A
+b: A
+or_assoc: forall A B C : Prop, (A \/ B) \/ C <-> A \/ B \/ C
+and_assoc: forall A B C : Prop, (A /\ B) /\ C <-> A /\ B /\ C
+eq_trans_assoc:
+  forall [A : Type] [x y z t : A] (e : x = y) (e' : y = z) (e'' : z = t),
+  eq_trans e (eq_trans e' e'') = eq_trans (eq_trans e e') e''
+plus_O_n: forall n : nat, 0 + n = n
+plus_n_O: forall n : nat, n = n + 0
+plus_n_Sm: forall n m : nat, S (n + m) = n + S m
+plus_Sn_m: forall n m : nat, S n + m = S (n + m)
+mult_n_Sm: forall n m : nat, n * m + n = n * S m
+f_equal2_plus:
+  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
+nat_rect_plus:
+  forall (n m : nat) {A : Type} (f : A -> A) (x : A),
+  nat_rect (fun _ : nat => A) x (fun _ : nat => f) (n + m) =
+  nat_rect (fun _ : nat => A)
+    (nat_rect (fun _ : nat => A) x (fun _ : nat => f) m) 
+    (fun _ : nat => f) n
+Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
+Numeral.internal_numeral_dec_bl:
+  forall x y : Numeral.numeral, Numeral.numeral_beq x y = true -> x = y
+Numeral.internal_int_dec_bl1:
+  forall x y : Numeral.int, Numeral.int_beq x y = true -> x = y
+Numeral.internal_uint_dec_bl1:
+  forall x y : Numeral.uint, Numeral.uint_beq x y = true -> x = y
+Hexadecimal.internal_hexadecimal_dec_bl:
+  forall x y : Hexadecimal.hexadecimal,
+  Hexadecimal.hexadecimal_beq x y = true -> x = y
+Hexadecimal.internal_int_dec_bl0:
+  forall x y : Hexadecimal.int, Hexadecimal.int_beq x y = true -> x = y
+Decimal.internal_decimal_dec_bl:
+  forall x y : Decimal.decimal, Decimal.decimal_beq x y = true -> x = y
+Decimal.internal_int_dec_bl:
+  forall x y : Decimal.int, Decimal.int_beq x y = true -> x = y
+Byte.of_bits:
+  bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) ->
+  Byte.byte
+Byte.to_bits_of_bits:
+  forall
+    b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))),
+  Byte.to_bits (Byte.of_bits b) = b
+Numeral.internal_numeral_dec_lb:
+  forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true
+Numeral.internal_uint_dec_lb1:
+  forall x y : Numeral.uint, x = y -> Numeral.uint_beq x y = true
+Numeral.internal_int_dec_lb1:
+  forall x y : Numeral.int, x = y -> Numeral.int_beq x y = true
+Decimal.internal_int_dec_lb:
+  forall x y : Decimal.int, x = y -> Decimal.int_beq x y = true
+Hexadecimal.internal_hexadecimal_dec_lb:
+  forall x y : Hexadecimal.hexadecimal,
+  x = y -> Hexadecimal.hexadecimal_beq x y = true
+Hexadecimal.internal_int_dec_lb0:
+  forall x y : Hexadecimal.int, x = y -> Hexadecimal.int_beq x y = true
+Decimal.internal_decimal_dec_lb:
+  forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true
+Byte.to_bits:
+  Byte.byte ->
+  bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))
+Hexadecimal.internal_uint_dec_bl0:
+  forall x : Hexadecimal.uint,
+  (fun x0 : Hexadecimal.uint =>
+   forall y : Hexadecimal.uint, Hexadecimal.uint_beq x0 y = true -> x0 = y) x
+Decimal.internal_uint_dec_lb:
+  forall x : Decimal.uint,
+  (fun x0 : Decimal.uint =>
+   forall y : Decimal.uint, x0 = y -> Decimal.uint_beq x0 y = true) x
+Decimal.internal_uint_dec_bl:
+  forall x : Decimal.uint,
+  (fun x0 : Decimal.uint =>
+   forall y : Decimal.uint, Decimal.uint_beq x0 y = true -> x0 = y) x
+Hexadecimal.internal_uint_dec_lb0:
+  forall x : Hexadecimal.uint,
+  (fun x0 : Hexadecimal.uint =>
+   forall y : Hexadecimal.uint, x0 = y -> Hexadecimal.uint_beq x0 y = true) x
+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
+Byte.to_bits_of_bits:
+  forall
+    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 x : S, {R1 x} + {R2 x}) ->
+  {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
+Nat.two: nat
+Nat.zero: nat
+Nat.one: nat
+Nat.succ: nat -> nat
+Nat.log2: nat -> nat
+Nat.sqrt: nat -> nat
+Nat.square: nat -> nat
+Nat.double: nat -> nat
+Nat.pred: nat -> nat
+Nat.ldiff: nat -> nat -> nat
+Nat.tail_mul: nat -> nat -> nat
+Nat.land: nat -> nat -> nat
+Nat.div: nat -> nat -> nat
+Nat.modulo: nat -> nat -> nat
+Nat.lor: nat -> nat -> nat
+Nat.lxor: nat -> nat -> nat
+Nat.of_hex_uint: Hexadecimal.uint -> nat
+Nat.of_uint: Decimal.uint -> nat
+Nat.of_num_uint: Numeral.uint -> nat
+length: forall [A : Type], list A -> nat
+plus_n_O: forall n : nat, n = n + 0
+plus_O_n: forall n : nat, 0 + n = n
+plus_n_Sm: forall n m : nat, S (n + m) = n + S m
+plus_Sn_m: forall n m : nat, S n + m = S (n + m)
+mult_n_Sm: forall n m : nat, n * m + n = n * S m
+Nat.land_comm: forall a b : nat, Nat.land a b = Nat.land b a
+Nat.lor_comm: forall a b : nat, Nat.lor a b = Nat.lor b a
+Nat.lxor_comm: forall a b : nat, Nat.lxor a b = Nat.lxor b a
+Nat.lcm_comm: forall a b : nat, Nat.lcm a b = Nat.lcm b a
+Nat.min_comm: forall n m : nat, Nat.min n m = Nat.min m n
+Nat.gcd_comm: forall n m : nat, Nat.gcd n m = Nat.gcd m n
+Bool.xorb_comm: forall b b' : bool, xorb b b' = xorb b' b
+Nat.max_comm: forall n m : nat, Nat.max n m = Nat.max m n
+Nat.mul_comm: forall n m : nat, n * m = m * n
+Nat.add_comm: forall n m : nat, n + m = m + n
+Bool.orb_comm: forall b1 b2 : bool, (b1 || b2)%bool = (b2 || b1)%bool
+Bool.andb_comm: forall b1 b2 : bool, (b1 && b2)%bool = (b2 && b1)%bool
+Nat.eqb_sym: forall x y : nat, (x =? y) = (y =? x)
+Nat.bit0_eqb: forall a : nat, Nat.testbit a 0 = (a mod 2 =? 1)
+Nat.land_ones: forall a n : nat, Nat.land a (Nat.ones n) = a mod 2 ^ n
+Nat.div_exact: forall a b : nat, b <> 0 -> a = b * (a / b) <-> a mod b = 0
+Nat.testbit_spec':
+  forall a n : nat, Nat.b2n (Nat.testbit a n) = (a / 2 ^ n) mod 2
+Nat.pow_div_l:
+  forall a b c : nat, b <> 0 -> a mod b = 0 -> (a / b) ^ c = a ^ c / b ^ c
+Nat.testbit_eqb: forall a n : nat, Nat.testbit a n = ((a / 2 ^ n) mod 2 =? 1)
+Nat.testbit_false:
+  forall a n : nat, Nat.testbit a n = false <-> (a / 2 ^ n) mod 2 = 0
+Nat.testbit_true:
+  forall a n : nat, Nat.testbit a n = true <-> (a / 2 ^ n) mod 2 = 1
+Nat.bit0_eqb: forall a : nat, Nat.testbit a 0 = (a mod 2 =? 1)
+Nat.land_ones: forall a n : nat, Nat.land a (Nat.ones n) = a mod 2 ^ n
+Nat.div_exact: forall a b : nat, b <> 0 -> a = b * (a / b) <-> a mod b = 0
+Nat.testbit_spec':
+  forall a n : nat, Nat.b2n (Nat.testbit a n) = (a / 2 ^ n) mod 2
+Nat.pow_div_l:
+  forall a b c : nat, b <> 0 -> a mod b = 0 -> (a / b) ^ c = a ^ c / b ^ c
+Nat.testbit_eqb: forall a n : nat, Nat.testbit a n = ((a / 2 ^ n) mod 2 =? 1)
+Nat.testbit_false:
+  forall a n : nat, Nat.testbit a n = false <-> (a / 2 ^ n) mod 2 = 0
+Nat.testbit_true:
+  forall a n : nat, Nat.testbit a n = true <-> (a / 2 ^ n) mod 2 = 1
+iff_Symmetric: Symmetric iff
+iff_Reflexive: Reflexive iff
+impl_Reflexive: Reflexive Basics.impl
+eq_Symmetric: forall {A : Type}, Symmetric eq
+eq_Reflexive: forall {A : Type}, Reflexive eq
+Equivalence_Symmetric:
+  forall {A : Type} {R : Relation_Definitions.relation A},
+  Equivalence R -> Symmetric R
+Equivalence_Reflexive:
+  forall {A : Type} {R : Relation_Definitions.relation A},
+  Equivalence R -> Reflexive R
+PER_Symmetric:
+  forall {A : Type} {R : Relation_Definitions.relation A},
+  PER R -> Symmetric R
+PreOrder_Reflexive:
+  forall {A : Type} {R : Relation_Definitions.relation A},
+  PreOrder R -> Reflexive R
+reflexive_eq_dom_reflexive:
+  forall {A B : Type} {R' : Relation_Definitions.relation B},
+  Reflexive R' -> Reflexive (eq ==> R')%signature
diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v
index 82096f29bf..4ec7a760b9 100644
--- a/test-suite/output/Search.v
+++ b/test-suite/output/Search.v
@@ -35,3 +35,34 @@ Goal forall n (P:nat -> Prop), P n -> ~P n -> False.
 
 Abort.
 
+Module M.
+Section S.
+Variable A:Type.
+Variable a:A.
+Theorem Thm (b:A) : True.
+Search A. (* Test search in hypotheses *)
+Abort.
+End S.
+End M.
+
+(* Reproduce the example of the doc *)
+
+Reset Initial.
+
+Search "_assoc".
+Search "+".
+Search hyp:bool -headhyp:bool.
+Search concl:bool -headconcl:bool.
+Search [ is:Definition headconcl:nat | is:Lemma (_ + _) ].
+
+Require Import PeanoNat.
+
+Search (_ ?n ?m = _ ?m ?n).
+Search "'mod'" -"mod".
+Search "mod"%nat -"mod".
+
+Reset Initial.
+
+Require Import Morphisms.
+
+Search is:Instance [ Reflexive | Symmetric ].
diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out
index d42dc575c2..9554581ebe 100644
--- a/test-suite/output/SearchHead.out
+++ b/test-suite/output/SearchHead.out
@@ -1,10 +1,17 @@
+File "stdin", line 3, characters 0-14:
+Warning:
+SearchHead is deprecated. Use the headconcl: clause of Search instead.
+[deprecated-searchhead,deprecated]
 le_n: forall n : nat, n <= n
 le_0_n: forall n : nat, 0 <= n
 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)
+File "stdin", line 4, characters 0-16:
+Warning:
+SearchHead is deprecated. Use the headconcl: clause of Search instead.
+[deprecated-searchhead,deprecated]
 false: bool
 true: bool
 negb: bool -> bool
@@ -28,7 +35,10 @@ 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)
+File "stdin", line 5, characters 0-21:
+Warning:
+SearchHead is deprecated. Use the headconcl: clause of Search instead.
+[deprecated-searchhead,deprecated]
 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 +57,13 @@ 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)
+File "stdin", line 11, characters 2-20:
+Warning:
+SearchHead is deprecated. Use the headconcl: clause of Search instead.
+[deprecated-searchhead,deprecated]
 h: newdef n
-(use "About" for full details on implicit arguments)
+File "stdin", line 17, characters 2-15:
+Warning:
+SearchHead is deprecated. Use the headconcl: clause of Search instead.
+[deprecated-searchhead,deprecated]
 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)