Ajout de tests

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

5 files changed, 105 insertions, 0 deletions

diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v
new file mode 100644
index 0000000000..ac6511bdf8
--- /dev/null
+++ b/test-suite/failure/clash_cons.v
@@ -0,0 +1,9 @@
+(* Teste la verification d'unicite des noms de constr *)
+
+
+Inductive X : Set := 
+    cons : X.
+
+Inductive Y : Set := 
+    cons : Y.
+
diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v
new file mode 100644
index 0000000000..3834fc0f52
--- /dev/null
+++ b/test-suite/success/fix.v
@@ -0,0 +1,44 @@
+(* Ancien bug signale par Laurent Thery sur la condition de garde *)
+
+Require Import Bool.
+Require Import ZArith.
+
+Definition rNat := positive.
+
+Inductive rBoolOp: Set :=
+     rAnd: rBoolOp
+    | rEq: rBoolOp .
+
+Definition rlt: rNat -> rNat ->Prop := [a, b:rNat](compare a b EGAL)=INFERIEUR.
+
+Definition rltDec: (m, n:rNat){(rlt m n)}+{(rlt n m) \/ m=n}.
+Intros n m; Generalize (compare_convert_INFERIEUR n m);
+ Generalize (compare_convert_SUPERIEUR n m);
+ Generalize (compare_convert_EGAL n m); Case (compare n m EGAL).
+Intros H' H'0 H'1; Right; Right; Auto.
+Intros H' H'0 H'1; Left; Unfold rlt.
+Apply convert_compare_INFERIEUR; Auto.
+Intros H' H'0 H'1; Right; Left; Unfold rlt.
+Apply convert_compare_INFERIEUR; Auto.
+Apply H'0; Auto.
+Defined.
+
+
+Definition rmax: rNat -> rNat ->rNat.
+Intros n m; Case (rltDec n m); Intros Rlt0.
+Exact m.
+Exact n.
+Defined.
+
+Inductive rExpr: Set :=
+     rV: rNat ->rExpr
+    | rN: rExpr ->rExpr
+    | rNode: rBoolOp -> rExpr -> rExpr ->rExpr .
+
+Fixpoint maxVar[e:rExpr]: rNat :=
+   Cases e of
+       (rV n) => n
+      | (rN p) => (maxVar p)
+      | (rNode n p q) => (rmax (maxVar p) (maxVar q))
+   end.
+
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
new file mode 100644
index 0000000000..cffc8ba7af
--- /dev/null
+++ b/test-suite/success/induct.v
@@ -0,0 +1,10 @@
+(* Teste des definitions inductives imbriquees *)
+
+Require PolyList.
+
+Inductive X : Set := 
+    cons1 : (list X)->X.
+
+Inductive Y : Set := 
+    cons2 : (list Y*Y)->Y.
+
diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v
new file mode 100644
index 0000000000..61d984eb46
--- /dev/null
+++ b/test-suite/success/mutual_ind.v
@@ -0,0 +1,34 @@
+(* Definition mutuellement inductive et dependante *)
+
+Require Export PolyList.
+
+ Record signature : Type := {
+    sort : Set;
+    sort_beq : sort->sort->bool;
+    sort_beq_refl : (f:sort)true=(sort_beq f f);
+    sort_beq_eq : (f1,f2:sort)true=(sort_beq f1 f2)->f1=f2;
+    fsym :> Set;
+    fsym_type : fsym->(list sort)*sort;
+    fsym_beq : fsym->fsym->bool;
+    fsym_beq_refl : (f:fsym)true=(fsym_beq f f);
+    fsym_beq_eq : (f1,f2:fsym)true=(fsym_beq f1 f2)->f1=f2
+  }.
+
+ 
+ Variable F : signature.
+
+  Definition vsym := (sort F)*nat.
+
+  Definition vsym_sort := (fst (sort F) nat).
+  Definition vsym_nat := (snd (sort F) nat).
+ 
+
+  Mutual Inductive term : (sort F)->Set :=
+  	| term_var : (v:vsym)(term (vsym_sort v))
+	| term_app : (f:F)(list_term (Fst (fsym_type F f)))
+		->(term (Snd (fsym_type F f)))
+  with list_term : (list (sort F)) -> Set :=
+	| term_nil : (list_term (nil (sort F)))
+	| term_cons : (s:(sort F);l:(list (sort F)))
+	  (term s)->(list_term l)->(list_term (cons s l)).
+
diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v
new file mode 100644
index 0000000000..59adcff237
--- /dev/null
+++ b/test-suite/success/unfold.v
@@ -0,0 +1,8 @@
+(* Test le Hint Unfold sur des var locales *)
+
+Section toto.
+Local EQ:=eq.
+Goal (EQ nat O O).
+Hints Unfold EQ.
+Auto.
+Save.