From: Ferruccio Guidi Date: Fri, 31 Mar 2017 12:11:23 +0000 (+0000) Subject: removed unused timeout flag X-Git-Tag: make_still_working~469 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ad7d22ea438c28a7f99726e0703cccbe2a8ba5b4;p=helm.git removed unused timeout flag --- diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml index b77c63369..1937229af 100644 --- a/matita/components/ng_tactics/nnAuto.ml +++ b/matita/components/ng_tactics/nnAuto.ml @@ -895,7 +895,6 @@ type flags = { maxwidth : int; maxsize : int; maxdepth : int; - timeout : float; } type cache = @@ -1833,7 +1832,6 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = maxwidth = width; maxsize = size; maxdepth = depth; - timeout = Unix.gettimeofday() +. 3000.; do_types = false; } in let initial_time = Unix.gettimeofday() in