diff options
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= |