From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 21 Oct 2009 14:52:00 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3265
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=01efa7df65c658be9b93dbefe3c2de0b8836fa5a;p=helm.git

...
---

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index c72550744..c9162d0fe 100644
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -1357,12 +1357,12 @@ let auto_tac ~params:(_univ,flags) status =
           timeout = Unix.gettimeofday() +. 3000.;
           do_types = false; 
   } in
-  let rec up_to x =
-    if x > depth then raise (Error (lazy "auto gave up", None))
+  let rec up_to x y =
+    if x > y then raise (Error (lazy "auto gave up", None))
     else
       let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
       match auto_main flags signature (elems x) cache with
-      | Gaveup -> up_to (x+1)
+      | Gaveup -> up_to (x+1) y
       | Proved (s, (_orlist, _cache)) -> 
           HLog.debug ("proved at depth " ^ string_of_int x);
           let stack = 
@@ -1372,7 +1372,7 @@ let auto_tac ~params:(_univ,flags) status =
           in
           s#set_stack stack
   in
-    up_to 2
+    up_to 2 depth
 ;;
 
 let group_by_tac eq_predicate tactic status = 
@@ -1392,8 +1392,7 @@ let group_by_tac eq_predicate tactic status =
   let classes = aux [] goals in
   List.iter 
    (fun l -> 
-      HLog.debug ("cluster:" ^
-          String.concat "," (List.map string_of_int l)))
+      HLog.debug ("cluster:" ^ String.concat "," (List.map string_of_int l)))
    classes;
   let pos_of l1 l2 = 
     let l2 = HExtlib.list_mapi (fun x i -> x,i+1) l2 in