Ajout de tests

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

1 files changed, 44 insertions, 0 deletions

diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v
new file mode 100644
index 000000000..3834fc0f5
--- /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.
+