diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-02-05 14:08:16 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-02-05 14:08:16 +0000 |
| commit | 36c0dbed2d5035c77cd1f2780269b95dc49a621c (patch) | |
| tree | 7e43b2c22c8be2e01c4395ec2e3e005d5a65285a | |
| parent | 80661ae35d42f16cc30581ec03c5550420637d40 (diff) | |
Suppression de l'élimination des existentiels dans LinearIntuition.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3663 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tauto.ml4 | 9 |
1 files changed, 6 insertions, 3 deletions
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>> |