From b7f2b98e90ba65984c7f0d24fcdaabf1d6af7270 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Tue, 6 Feb 2001 12:18:57 +0000
Subject: Ajout d'un exemple

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

diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v
index fc1ee0fca6..0dbed8ffad 100644
--- a/test-suite/success/Tauto.v
+++ b/test-suite/success/Tauto.v
@@ -122,7 +122,7 @@ Proof.
   Tauto.
 Save.
 
-(* This example takes much time with the old version of Tauto *)
+(* This example took much time with the old version of Tauto *)
 Lemma critical_example0:(~~B->B)->(A->B)->~~A->B.
 Proof.
   Tauto.
@@ -134,6 +134,13 @@ Proof.
   Tauto.
 Save.
 
+(* This example took very much time (about 3mn on a PIII 450MHz in bytecode)
+   with the old Tauto. Now, it's immediate (less than 1s). *)
+Lemma critical_example2:(~A<->B)->(~B<->A)->(~~A<->A).
+Proof.
+  Tauto.
+Save.
+
 (* An example which was a bug *)
 Lemma old_bug:(~A<->B)->(~(C\/E)<->D/\F)->~(C\/A\/E)<->D/\B/\F.
 Proof.
-- 
cgit v1.2.3