From c8b567cf0317fb30a907444b11866121416168e1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Oct 2009 13:27:48 +0000 Subject: [PATCH] better logging --- helm/software/components/ng_tactics/nAuto.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml index 525e1bfb6..50558eb39 100644 --- a/helm/software/components/ng_tactics/nAuto.ml +++ b/helm/software/components/ng_tactics/nAuto.ml @@ -1193,7 +1193,7 @@ let intro_case status gno gty depth cache name = let t = mk_cic_term ctx (NCic.Rel 1) in let status, keys = keys_of_term status t in let cache = List.fold_left (add_to_th t) cache keys in - debug_print (lazy (" intro: "^ string_of_int open_goal)); + debug_print ~depth (lazy ("intro: "^ string_of_int open_goal)); incr candidate_no; (* XXX calculate the sort *) [(!candidate_no,Ast.Implicit `JustOne),0,status,[open_goal,P]], @@ -1277,7 +1277,7 @@ let auto_main flags signature (pos : 'a and_pos) cache = in let rec next ~unfocus (pos : 'a and_pos) cache = - (* USER HINT *) + (* TODO: process USER HINT is any *) match Z.downA pos with | Z.Unexplored -> attack pos cache (Z.getA pos) | Z.Alternatives pos -> nextO ~unfocus pos cache @@ -1308,7 +1308,7 @@ let auto_main flags signature (pos : 'a and_pos) cache = | (_, size, depth), S (g,_) (* S if already solved and then solved again because of a backtrack *) | (_, size, depth), D g -> - let newg = S (g,status) in(* TODO: cache success g *) + let newg = S (g,status) in (* TODO: cache success g *) let status = if unfocus then NTactics.unfocus_tac status else status in let news = status,size,depth in let pos = Z.setA news newg pos in -- 2.39.2