diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-28 13:30:24 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-28 13:30:24 +0000 |
| commit | 49db22be8b253900362f210ebd800ba1d326e589 (patch) | |
| tree | d7e9a593bed9bc4301710038ca27870a6f5442ca /tactics/newtauto.ml4 | |
| parent | 3d29ae897bd291994a81df69096be3dfee17c418 (diff) | |
Fixed Relative names not,iff in Camlp4 quotation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3799 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/newtauto.ml4')
| -rw-r--r-- | tactics/newtauto.ml4 | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/tactics/newtauto.ml4 b/tactics/newtauto.ml4 index f378bbe80..04ecc36fa 100644 --- a/tactics/newtauto.ml4 +++ b/tactics/newtauto.ml4 @@ -56,10 +56,7 @@ let isrec ind= let (mib,mip) = Global.lookup_inductive ind in Inductiveops.mis_is_recursive (ind,mib,mip) -let simplif=interp - <:tactic<Repeat (Match Context With - |[|- ?]->Progress Unfold not iff - |[H:?|- ?]->Progress Unfold not iff in H)>> +let simplif=Tauto.reduction_not_iff let rule_axiom=assumption @@ -207,9 +204,7 @@ let q_elim tac= let vtac=Tacexpr.TacArg (valueIn (VTactic tac)) in interp <:tactic< Match Context With - [x:?1|-(? ?1 ?)]-> - Exists x;$vtac - |[x:?1;H:?1->?|-?]-> + [x:?1;H:?1->?|-?]-> Generalize (H x);Clear H;$vtac>> let rec lfo n= |