From c74b914b3e4614e273cbe2c27df87d91a70cd8a6 Mon Sep 17 00:00:00 2001
From: courant
Date: Fri, 19 Jul 2002 15:06:11 +0000
Subject: correction bugs Tauto

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2905 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/Tauto.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v
index bbc67f6696..3afe7a6bc2 100644
--- a/test-suite/success/Tauto.v
+++ b/test-suite/success/Tauto.v
@@ -179,6 +179,13 @@ Proof.
   Tauto.
 Save.
 
+(* sometimes, the behaviour of Tauto depends on the order of the hyps *)
+Lemma old_bug3bis:
+  ~((A->B)->B)->((~B\/~B)/\(~B\/~A)/\(B\/~B)/\(B\/~A)->False)->False.
+Proof.
+  Tauto.
+Save.
+
 (* A bug found by Freek Wiedijk <freek@cs.kun.nl> *)
 Lemma new_bug:
  ((A<->B)->(B<->C)) ->
@@ -189,6 +196,7 @@ Proof.
   Tauto.
 Save.
 
+
 (*  A private club has the following rules :
  *
  *  . rule 1 : Every non-scottish member wears red socks
@@ -229,3 +237,4 @@ Lemma intu1:((A:Prop)A\/~A)->(x,y:nat)(x=y\/~x=y).
 Proof.
   Intuition.
 Save.
+
-- 
cgit v1.2.3