diff options
| -rw-r--r-- | test-suite/success/Tauto.v | 9 |
1 files changed, 8 insertions, 1 deletions
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. |