From 36c0dbed2d5035c77cd1f2780269b95dc49a621c Mon Sep 17 00:00:00 2001
From: corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 5 Feb 2003 14:08:16 +0000
Subject: Suppression de l'élimination des existentiels dans LinearIntuition.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3663 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tauto.ml4 | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 848ba16e0..d57b4c2ac 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -153,9 +153,7 @@ let default_intuition_tac = <:tactic< Auto with * >>
 let q_elim tac=
   <:tactic<
   Match Context With 
-    [x:?1|-(? ?1 ?)]->
-      Exists x;$tac
-  |[x:?1;H:?1->?|-?]->
+  [x:?1;H:?1->?|-?]->
       Generalize (H x);Clear H;$tac>>
 
 let rec lfo n gl=
@@ -188,3 +186,8 @@ TACTIC EXTEND LinearIntuition
 | [ "LinearIntuition" integer(n)] -> [ lfo_wrap n]
 END
 
+TACTIC EXTEND Test
+| [ "Test" ] -> [ reduction_not_iff ]
+END
+
+let default =interp <:tactic<Test>>
-- 
cgit v1.2.3