Ajout du test de Tauto

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

1 files changed, 19 insertions, 0 deletions

diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v
new file mode 100644
index 000000000..2c147895c
--- /dev/null
+++ b/test-suite/failure/Tauto.v
@@ -0,0 +1,19 @@
+(**** Tactics Tauto and Intuition ****)
+
+(**** Tauto:
+  Tactic for automating proof in Intuionnistic Propositional Calculus, based on
+  the contraction-free LJT of Dickhoff ****)
+
+(**** 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.
+Proof.
+  Tauto.