From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 12 Oct 2006 13:34:32 +0000 (+0000)
Subject: timeout if unspecfied should be set to infinity, not 0, since the timeout inside... 
X-Git-Tag: 0.4.95@7852~896
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ece1b63a7eec3567ef9eda9bcd1550655a575d07;p=helm.git

timeout if unspecfied should be set to infinity, not 0, since the timeout inside the flagfs structure is a time in the future, not a decreasing quantity.
every loop of auto the check gettimeofday() > timeout raise Fail
---

diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml
index 4acacefc6..b904d52cb 100644
--- a/components/tactics/auto.ml
+++ b/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 ***********)
 
@@ -571,7 +571,7 @@ let flags_of_params params ?(for_applyS=false) () =
       if timeout = 0 then
        if for_applyS then Unix.gettimeofday () +. 30.0
        else
-        0.0
+         infinity
       else
        Unix.gettimeofday() +. (float_of_int timeout); 
     AutoTypes.use_paramod = use_paramod;