X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=b904d52cb055bcd22263eee84d67108da633e54b;hb=1f829cda7957b48cac8109a3721ded11f6cec8de;hp=305a42ab1adfab718e77d1e4d8f33bd7b919045e;hpb=46834f1afe49d481045a40fb1bf6ddbddcfef9f5;p=helm.git

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 305a42ab1..b904d52cb 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -26,7 +26,7 @@
 open AutoTypes;;
 open AutoCache;;
 
-let debug_print s = () (*prerr_endline s;;*)
+let debug_print s = () (* prerr_endline s;; *)
 
 (* {{{ *********** local given_clause wrapper ***********)
 
@@ -555,10 +555,12 @@ let int params name default =
         raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
 ;;  
 
-let flags_of_params params ?(use_only_paramod = bool params "paramodulation" false) () =
+let flags_of_params params ?(for_applyS=false) () =
  let int = int params in
  let bool = bool params in
  let use_paramod = bool "use_paramod" true in
+ let use_only_paramod =
+  if for_applyS then true else bool "paramodulation" false in
  let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
  let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
  let timeout = int "timeout" 0 in
@@ -567,9 +569,9 @@ let flags_of_params params ?(use_only_paramod = bool params "paramodulation" fal
     AutoTypes.maxwidth = width;
     AutoTypes.timeout = 
       if timeout = 0 then
-       if use_only_paramod then Unix.gettimeofday () +. 30.0
+       if for_applyS then Unix.gettimeofday () +. 30.0
        else
-        0.0
+         infinity
       else
        Unix.gettimeofday() +. (float_of_int timeout); 
     AutoTypes.use_paramod = use_paramod;
@@ -583,7 +585,7 @@ let applyS_tac ~dbd ~term ~params =
     try 
       let _, proof, gl,_,_ =
        apply_smart ~dbd ~term ~subst:[]
-        (flags_of_params params ~use_only_paramod:true ()) status
+        (flags_of_params params ~for_applyS:true ()) status
       in 
        proof, gl
     with