Ajout de deux anciens bugs

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

1 files changed, 17 insertions, 2 deletions

diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v
index 3b5e90fad..6e8bf0f14 100644
--- a/test-suite/success/Tauto.v
+++ b/test-suite/success/Tauto.v
@@ -151,8 +151,23 @@ Proof.
   Tauto.
 Save.
 
-(* An example which was a bug *)
-Lemma old_bug:(~A<->B)->(~(C\/E)<->D/\F)->~(C\/A\/E)<->D/\B/\F.
+(* This example was a bug *)
+Lemma old_bug0:(~A<->B)->(~(C\/E)<->D/\F)->~(C\/A\/E)<->D/\B/\F.
+Proof.
+  Tauto.
+Save.
+
+(* Another bug *)
+Lemma old_bug1:((A->B->False)->False) -> (B->False) -> False.
+Proof.
+  Tauto.
+Save.
+
+(* A bug again *)
+Lemma old_bug2:
+  ((((C->False)->A)->((B->False)->A)->False)->False) ->
+  (((C->B->False)->False)->False) ->
+  ~A->A.
 Proof.
   Tauto.
 Save.