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