From 239e24b749014df5fbd83663ba4e865ab8e81db0 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Fri, 5 Jul 2002 11:58:31 +0000
Subject: Added a new uncompleteness bug found in Tauto.

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

diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v
index ecaaf80d4f..f751d52bf0 100644
--- a/test-suite/success/Tauto.v
+++ b/test-suite/success/Tauto.v
@@ -179,6 +179,16 @@ Proof.
   Tauto.
 Save.
 
+(* A bug found by Freek Wiedijk <freek@cs.kun.nl> *)
+Lemma new_bug:
+Goal ((A<->B)->(B<->C)) ->
+     ((B<->C)->(C<->A)) ->
+     ((C<->A)->(A<->B)) ->
+     (A<->B).
+Proof.
+  Tauto.
+Save.
+
 (*  A private club has the following rules :
  *
  *  . rule 1 : Every non-scottish member wears red socks
-- 
cgit v1.2.3