From 01efa7df65c658be9b93dbefe3c2de0b8836fa5a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 21 Oct 2009 14:52:00 +0000 Subject: [PATCH 1/1] ... --- helm/software/components/ng_tactics/nAuto.ml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) 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 -- 2.39.2