diff options
| -rw-r--r-- | tactics/newtauto.ml4 | 9 | ||||
| -rw-r--r-- | tactics/tauto.ml4 | 21 |
2 files changed, 14 insertions, 16 deletions
diff --git a/tactics/newtauto.ml4 b/tactics/newtauto.ml4 index f378bbe803..04ecc36fa2 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= diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 2a0a01f43d..36ee7e18a6 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -52,12 +52,12 @@ let not_dep_intros ist = Repeat Match Context With | [|- ?1 -> ?2 ] -> Intro -| [|- (iff ? ?)] -> Unfold iff -| [|- (not ?)] -> Unfold not -| [ H:(iff ? ?)|- ?] -> Unfold iff in H -| [ H:(not ?)|-?] -> Unfold not in H -| [ H:(iff ? ?)->?|- ?] -> Unfold iff in H -| [ H:(not ?)->?|-?] -> Unfold not in H >> +| [|- (Coq.Init.Logic.iff ? ?)] -> Unfold Coq.Init.Logic.iff +| [|- (Coq.Init.Logic.not ?)] -> Unfold Coq.Init.Logic.not +| [ H:(Coq.Init.Logic.iff ? ?)|- ?] -> Unfold Coq.Init.Logic.iff in H +| [ H:(Coq.Init.Logic.not ?)|-?] -> Unfold Coq.Init.Logic.not in H +| [ H:(Coq.Init.Logic.iff ? ?)->?|- ?] -> Unfold Coq.Init.Logic.iff in H +| [ H:(Coq.Init.Logic.not ?)->?|-?] -> Unfold Coq.Init.Logic.not in H >> let axioms ist = let t_is_unit = tacticIn is_unit @@ -136,9 +136,12 @@ let rec tauto_intuit t_reduce t_solver ist = ) >> let reduction_not_iff=interp - <:tactic<Repeat (Match Context With - |[|- ?]->Progress Unfold not iff - |[H:?|- ?]->Progress Unfold not iff in H)>> + <:tactic<Repeat + (Match Context With + |[|- ?]-> + Progress Unfold Coq.Init.Logic.not Coq.Init.Logic.iff + |[H:?|- ?]-> + Progress Unfold Coq.Init.Logic.not Coq.Init.Logic.iff in H)>> let t_reduction_not_iff = Tacexpr.TacArg (valueIn (VTactic reduction_not_iff)) |