diff options
| -rw-r--r-- | tactics/tauto.ml4 | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 6b90f3f000..4546f29f7c 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -104,13 +104,23 @@ let compute = function let reduction = Tacticals.onAllClauses (fun ido -> compute ido) +(* As a simple heuristic, first we try to avoid reduction both in *) +(* tauto and intuition *) + let tauto = (tclTHEN (init_intros ()) - (tclTHEN reduction (interp (tauto_main ())))) + (tclORELSE + (interp (tauto_main ())) + (tclTHEN reduction (interp (tauto_main ())))) + ) let intuition = - (tclTHEN (init_intros ()) - (tclTHEN reduction (interp (intuition_main ())))) + tclTHEN (init_intros ()) + (tclORELSE + (interp (intuition_main ())) + (tclTHEN reduction (interp (intuition_main ()))) + ) + let _ = hide_atomic_tactic "Tauto" tauto let _ = hide_atomic_tactic "Intuition" intuition |