Minimal test suite for search commands

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12860 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 120 insertions, 0 deletions

diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
new file mode 100644
index 0000000000..93eff64c90
--- /dev/null
+++ b/test-suite/output/Search.out
@@ -0,0 +1,42 @@
+le_S: forall n m : nat, n <= m -> n <= S m
+le_n: forall n : nat, n <= n
+le_pred: forall n m : nat, n <= m -> pred n <= pred m
+le_S_n: forall n m : nat, S n <= S m -> n <= m
+false: bool
+true: bool
+sumor_beq:
+  forall (A : Type) (B : Prop),
+  (A -> A -> bool) -> (B -> B -> bool) -> A + {B} -> A + {B} -> bool
+sumbool_beq:
+  forall A B : Prop,
+  (A -> A -> bool) -> (B -> B -> bool) -> {A} + {B} -> {A} + {B} -> bool
+xorb: bool -> bool -> bool
+sum_beq:
+  forall A B : Type,
+  (A -> A -> bool) -> (B -> B -> bool) -> A + B -> A + B -> bool
+prod_beq:
+  forall A B : Type,
+  (A -> A -> bool) -> (B -> B -> bool) -> A * B -> A * B -> bool
+orb: bool -> bool -> bool
+option_beq: forall A : Type, (A -> A -> bool) -> option A -> option A -> bool
+negb: bool -> bool
+nat_beq: nat -> nat -> bool
+list_beq: forall A : Type, (A -> A -> bool) -> list A -> list A -> bool
+implb: bool -> bool -> bool
+comparison_beq: comparison -> comparison -> bool
+bool_beq: bool -> bool -> bool
+andb: bool -> bool -> bool
+Empty_set_beq: Empty_set -> Empty_set -> bool
+pred_Sn: forall n : nat, n = pred (S n)
+plus_n_Sm: forall n m : nat, S (n + m) = n + S m
+plus_n_O: forall n : nat, n = n + 0
+plus_Sn_m: forall n m : nat, S n + m = S (n + m)
+plus_O_n: forall n : nat, 0 + n = n
+mult_n_Sm: forall n m : nat, n * m + n = n * S m
+mult_n_O: forall n : nat, 0 = n * 0
+min_r: forall n m : nat, m <= n -> min n m = m
+min_l: forall n m : nat, n <= m -> min n m = n
+max_r: forall n m : nat, n <= m -> max n m = m
+max_l: forall n m : nat, m <= n -> max n m = n
+eq_add_S: forall n m : nat, S n = S m -> n = m
+eq_S: forall x y : nat, x = y -> S x = S y
diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v
new file mode 100644
index 0000000000..f1489f22ae
--- /dev/null
+++ b/test-suite/output/Search.v
@@ -0,0 +1,5 @@
+(* Some tests of the Search command *)
+
+Search le.				(* app nodes *)
+Search bool. 				(* no apps *)
+Search (@eq nat).			(* complex pattern *)
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
new file mode 100644
index 0000000000..0c32f8d8d9
--- /dev/null
+++ b/test-suite/output/SearchPattern.out
@@ -0,0 +1,48 @@
+false: bool
+true: bool
+sumor_beq:
+  forall (A : Type) (B : Prop),
+  (A -> A -> bool) -> (B -> B -> bool) -> A + {B} -> A + {B} -> bool
+sumbool_beq:
+  forall A B : Prop,
+  (A -> A -> bool) -> (B -> B -> bool) -> {A} + {B} -> {A} + {B} -> bool
+xorb: bool -> bool -> bool
+sum_beq:
+  forall A B : Type,
+  (A -> A -> bool) -> (B -> B -> bool) -> A + B -> A + B -> bool
+prod_beq:
+  forall A B : Type,
+  (A -> A -> bool) -> (B -> B -> bool) -> A * B -> A * B -> bool
+orb: bool -> bool -> bool
+option_beq: forall A : Type, (A -> A -> bool) -> option A -> option A -> bool
+negb: bool -> bool
+nat_beq: nat -> nat -> bool
+list_beq: forall A : Type, (A -> A -> bool) -> list A -> list A -> bool
+implb: bool -> bool -> bool
+comparison_beq: comparison -> comparison -> bool
+bool_beq: bool -> bool -> bool
+andb: bool -> bool -> bool
+Empty_set_beq: Empty_set -> Empty_set -> bool
+S: nat -> nat
+O: nat
+pred: nat -> nat
+plus: nat -> nat -> nat
+mult: nat -> nat -> nat
+minus: nat -> nat -> nat
+min: nat -> nat -> nat
+max: nat -> nat -> nat
+length: forall A : Type, list A -> nat
+S: nat -> nat
+pred: nat -> nat
+plus: nat -> nat -> nat
+mult: nat -> nat -> nat
+minus: nat -> nat -> nat
+min: nat -> nat -> nat
+max: nat -> nat -> nat
+mult_n_Sm: forall n m : nat, n * m + n = n * S m
+le_n: forall n : nat, n <= n
+eq_refl: forall (A : Type) (x : A), x = x
+identity_refl: forall (A : Type) (a : A), identity a a
+iff_refl: forall A : Prop, A <-> A
+conj: forall A B : Prop, A -> B -> A /\ B
+pair: forall A B : Type, A -> B -> A * B
diff --git a/test-suite/output/SearchPattern.v b/test-suite/output/SearchPattern.v
new file mode 100644
index 0000000000..802d8c9760
--- /dev/null
+++ b/test-suite/output/SearchPattern.v
@@ -0,0 +1,19 @@
+(* Some tests of the SearchPattern command *)
+
+(* Simple, random tests *)
+SearchPattern bool.
+SearchPattern nat.
+SearchPattern le.
+
+(* With some hypothesis *)
+SearchPattern (nat -> nat).
+SearchPattern (?n * ?m + ?n = ?n * S ?m).
+
+(* Non-linearity *)
+SearchPattern (_ ?X ?X).
+
+(* Non-linearity with hypothesis *)
+SearchPattern (forall (x:?A) (y:?B), _ ?A ?B).
+
+(* No delta-reduction *)
+SearchPattern (Exc _).
diff --git a/test-suite/output/SearchRewrite.out b/test-suite/output/SearchRewrite.out
new file mode 100644
index 0000000000..f87aea1c84
--- /dev/null
+++ b/test-suite/output/SearchRewrite.out
@@ -0,0 +1,2 @@
+plus_n_O: forall n : nat, n = n + 0
+plus_O_n: forall n : nat, 0 + n = n
diff --git a/test-suite/output/SearchRewrite.v b/test-suite/output/SearchRewrite.v
new file mode 100644
index 0000000000..171a7363fe
--- /dev/null
+++ b/test-suite/output/SearchRewrite.v
@@ -0,0 +1,4 @@
+(* Some tests of the SearchRewrite command *)
+
+SearchRewrite (_+0). 			(* left *)
+SearchRewrite (0+_). 			(* right *)