Correction d'un bug dans check + ajout de tests

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

4 files changed, 129 insertions, 2 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/1411.v b/test-suite/bugs/closed/shouldsucceed/1411.v
new file mode 100644
index 0000000000..2ac7454b0c
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1411.v
@@ -0,0 +1,29 @@
+Require Import List.
+
+Inductive Tree : Set :=
+| Br : Tree -> Tree -> Tree
+| No : nat -> Tree
+.
+
+(* given a tree, we want to know which lists can
+   be used to navigate exactly to a node *)
+Inductive Exact : Tree -> list bool -> Prop :=
+| exDone  n    :              Exact (No n)   nil
+| exLeft  l r p: Exact l p -> Exact (Br l r) (true::p)
+| exRight l r p: Exact r p -> Exact (Br l r) (false::p)
+.
+
+Definition unreachable A : False -> A.
+intros.
+destruct H.
+Defined.
+
+Program Fixpoint fetch t p (x:Exact t p) {struct x} :=
+   match t, p with
+   | No p' , nil      => p'
+   | No p' , _::_     => unreachable nat _
+   | Br l r, nil      => unreachable nat _ 
+   | Br l r, true::t  => fetch l t _
+   | Br l r, false::t => fetch r t _
+   end.
+
diff --git a/test-suite/bugs/opened/shouldnotfail/1449.v b/test-suite/bugs/opened/shouldnotfail/1449.v
new file mode 100644
index 0000000000..d9695360f9
--- /dev/null
+++ b/test-suite/bugs/opened/shouldnotfail/1449.v
@@ -0,0 +1,5 @@
+Require Import Arith.
+
+Goal 0 <= 0.
+  eapply le_trans.
+  setoid_rewrite mult_comm.
diff --git a/test-suite/bugs/opened/shouldnotfail/1501.v b/test-suite/bugs/opened/shouldnotfail/1501.v
new file mode 100644
index 0000000000..85c09dbd14
--- /dev/null
+++ b/test-suite/bugs/opened/shouldnotfail/1501.v
@@ -0,0 +1,93 @@
+Set Implicit Arguments.
+
+
+Require Export Relation_Definitions.
+Require Export Setoid.
+
+
+Section Essais.
+
+(* Parametrized Setoid *)
+Parameter K : Type -> Type. 
+Parameter equiv : forall A : Type, K A -> K A -> Prop.
+Parameter equiv_refl : forall (A : Type) (x : K A), equiv x x.
+Parameter equiv_sym : forall (A : Type) (x y : K A), equiv x y -> equiv y x.
+Parameter equiv_trans : forall (A : Type) (x y z : K A), equiv x y -> equiv y z
+-> equiv x z.
+
+(* basic operations *)
+Parameter val : forall A : Type, A -> K A.
+Parameter bind : forall A B : Type, K A -> (A -> K B) -> K B.
+
+Parameter
+  bind_compat :
+    forall (A B : Type) (m1 m2 : K A) (f1 f2 : A -> K B),
+    equiv m1 m2 ->
+    (forall x : A, equiv (f1 x) (f2 x)) -> equiv (bind m1 f1) (bind m2 f2).
+
+(* monad axioms *)
+Parameter
+  bind_val_l :
+    forall (A B : Type) (a : A) (f : A -> K B), equiv (bind (val a) f) (f a).
+Parameter
+  bind_val_r :
+    forall (A : Type) (m : K A), equiv (bind m (fun a => val a)) m.
+Parameter
+  bind_assoc :
+    forall (A B C : Type) (m : K A) (f : A -> K B) (g : B -> K C),
+    equiv (bind (bind m f) g) (bind m (fun a => bind (f a) g)).
+
+
+Hint Resolve equiv_refl equiv_sym equiv_trans: monad.
+
+Add Relation K equiv 
+ reflexivity proved by (@equiv_refl)
+ symmetry proved by (@equiv_sym)
+ transitivity proved by (@equiv_trans)
+ as equiv_rel.
+
+Definition fequiv (A B: Type)  (f g: A -> K B) := forall (x:A), (equiv (f x) (g
+x)).
+
+Lemma fequiv_refl : forall (A B: Type) (f : A -> K B), fequiv f f.
+Proof.
+  unfold fequiv; auto with monad.
+Qed.
+
+Lemma fequiv_sym : forall (A B: Type) (x y : A -> K B), fequiv x y -> fequiv y
+x.
+Proof.
+  unfold fequiv; auto with monad.
+Qed.
+
+Lemma fequiv_trans : forall (A B: Type) (x y z : A -> K B), fequiv x y ->
+fequiv
+y z -> fequiv x z.
+Proof.
+  unfold fequiv; intros; eapply equiv_trans; auto with monad.
+Qed.
+
+Add Relation (fun (A B:Type) => A -> K B) fequiv 
+ reflexivity proved by (@fequiv_refl)
+ symmetry proved by (@fequiv_sym)
+ transitivity proved by (@fequiv_trans)
+ as fequiv_rel.
+
+Add Morphism bind
+ with signature equiv ==> fequiv ==> equiv
+ as bind_mor.
+Proof.
+ unfold fequiv; intros; apply bind_compat; auto.
+Qed.
+
+Lemma test:
+  forall (A B: Type) (m1 m2 m3: K A) (f: A -> A -> K B),
+ (equiv m1 m2) -> (equiv m2 m3) -> 
+   equiv (bind m1 (fun a => bind m2 (fun a' => f a a')))
+         (bind m2 (fun a => bind m3 (fun a' => f a a'))).
+Proof.
+  intros A B m1 m2 m3 f H1 H2. 
+  setoid_rewrite H1. (* this works *)
+  setoid_rewrite H2.
+  trivial by equiv_refl.
+Qed. 
diff --git a/test-suite/check b/test-suite/check
index b8577dee48..dd51c1e76c 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -198,7 +198,7 @@ test_bugs () {
 
 
     # At last, we test closed bugs that should fail
-    files=`/bin/ls -1 $1/bugs/closed/shouldfail/*.v 2> /dev/null`
+    files=`/bin/ls -1 $1/closed/shouldfail/*.v 2> /dev/null`
     for f in $files; do 
 	nbtests=`expr $nbtests + 1`
 	printf "    "$f"..."
@@ -207,7 +207,7 @@ test_bugs () {
 	    echo "Ok"
 	    nbtestsok=`expr $nbtestsok + 1`
         else 
-	    echo "Error! (bug seems to be opend, please check)"
+	    echo "Error! (bug seems to be opened, please check)"
         fi 
     done