Pas d'Apply dans Tauto

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1323 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 8 deletions

diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v
index 2c147895c..3e8bbeeb1 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.