...

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index c72550744669ada0ef27a88540f8f71f801c34e3..c9162d0fe2080923a5f31deca1fd5ffb5ff7c626 100644 (file)
--- 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