Test new Search features.

2 files changed, 190 insertions, 0 deletions

diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 43f4ed13d9..317e9c3757 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -287,3 +287,171 @@ h: P n
 h: P n
 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 08245a4a91..4ec7a760b9 100644
--- a/test-suite/output/Search.v
+++ b/test-suite/output/Search.v
@@ -44,3 +44,25 @@ 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 ].