From bbf12f80ac230a3fc9bea0f629f9f7bc6f5c44d3 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Mon, 5 Feb 2001 16:23:02 +0000
Subject: Pas d'Apply dans Tauto

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

diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v
index 2c147895c3..3e8bbeeb17 100644
--- a/test-suite/failure/Tauto.v
+++ b/test-suite/failure/Tauto.v
@@ -7,13 +7,7 @@
 (**** Intuition:
   Simplifications of goals, based on LJT calcul ****)
 
-(**** Introduction heuristic w.r.t. the dependent products:
- - Initially: Intros until the first non-dependent product and Intros of all
-   the non-dependent products
- - In the algorithm: Intros only the non-dependent products ****)
-
-(* Fails because False is after a dependent product which is after a
-   non-dependent product *)
-Goal (x,y:nat)x=y->(z:nat)False->x=z.
+(* Fails because Tauto does not perform any Apply *)
+Goal ((A:Prop)A\/~A)->(x,y:nat)(x=y\/~x=y).
 Proof.
   Tauto.
-- 
cgit v1.2.3