From 9d118318b1d0f664c1ccbcac06c8c279c3b8558d Mon Sep 17 00:00:00 2001
From: corbinea
Date: Fri, 5 Jul 2002 12:13:06 +0000
Subject: *** empty log message ***

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

diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v
index f751d52bf0..bbc67f6696 100644
--- a/test-suite/success/Tauto.v
+++ b/test-suite/success/Tauto.v
@@ -181,10 +181,10 @@ 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).
+ ((A<->B)->(B<->C)) ->
+ ((B<->C)->(C<->A)) ->
+ ((C<->A)->(A<->B)) ->
+ (A<->B).
 Proof.
   Tauto.
 Save.
-- 
cgit v1.2.3