better logging

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