As an heuristic, now both in tauto and intuition we try to avoid the initial

reduction


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1287 85f007b7-540e-0410-9357-904b9bb8a0f7

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