From 686b7d347ba8dc9a4e032cd4c6cb38da93c38188 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Fri, 15 Jun 2001 21:54:45 +0000
Subject: Fix d'un bug de Tauto

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

(limited to 'test-suite')

diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v
index 6e8bf0f140..ecaaf80d4f 100644
--- a/test-suite/success/Tauto.v
+++ b/test-suite/success/Tauto.v
@@ -172,6 +172,13 @@ Proof.
   Tauto.
 Save.
 
+(* A bug from CNF form *)
+Lemma old_bug3:
+  ((~A\/B)/\(~B\/B)/\(~A\/~B)/\(~B\/~B)->False)->~((A->B)->B)->False.
+Proof.
+  Tauto.
+Save.
+
 (*  A private club has the following rules :
  *
  *  . rule 1 : Every non-scottish member wears red socks
-- 
cgit v1.2.3