diff options
| author |  delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-06 12:18:57 +0000 |
|---|---|---|
| committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-06 12:18:57 +0000 |
| commit | b7f2b98e90ba65984c7f0d24fcdaabf1d6af7270 (patch) | |
| tree | 99f5309bc050efeeb5db29a8f067a99e1e706d99 /test-suite/success/Tauto.v | |
| parent | dd528e9c8bb70151e244a450539aea33adbe7c05 (diff) | |
Ajout d'un exemple
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1335 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/Tauto.v')
| -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 fc1ee0fca..0dbed8ffa 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. |