Debugging code is now controlled by the debug flag.

[helm.git] / components / tactics / autoTactic.ml

diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml
index 25696d7945448532efe981a56979a6bb61398320..8e94bba86e4f072796f32d482f363d5df2e5ed24 100644 (file)
--- a/components/tactics/autoTactic.ml
+++ b/components/tactics/autoTactic.ml
@@ -286,7 +286,7 @@ let auto_tac_old ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd)
         debug_print (lazy "AUTO_TAC HA FINITO");
         let _,_,p,_ = proof in
         debug_print (lazy (CicPp.ppterm p));
-        Printf.printf "tempo: %.9f\n" (t2 -. t1);
+        debug_print (lazy (Printf.sprintf "tempo: %.9f\n" (t2 -. t1)));
         (proof,[])
     | _ -> assert false
   in
@@ -322,6 +322,8 @@ let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) =
   let int = int params in
   let bool = bool params in
   let newauto = bool "new" false in
+  let use_only_paramod = bool "paramodulation" false in
+  let newauto = if use_only_paramod then true else newauto in
   let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
   let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
    if not newauto then