more printings

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index 8506c3adbdef5494c0081b0f5e8715daa4b189be..c72550744669ada0ef27a88540f8f71f801c34e3 100644 (file)
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -1335,6 +1335,15 @@ let auto_tac ~params:(_univ,flags) status =
   let goals = head_goals status#stack in
   let status, cache = mk_th_cache status goals in
 (*   pp_th status cache; *)
+(*
+  NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t -> 
+    debug_print (lazy(
+      NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
+      String.concat "\n    " (List.map (
+      NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[])
+        (NDiscriminationTree.TermSet.elements t))
+      )));
+*)
   let depth = int "depth" flags 3 in 
   let size  = int "size" flags 10 in 
   let width = int "width" flags (3+List.length goals) in 
@@ -1351,6 +1360,7 @@ let auto_tac ~params:(_univ,flags) status =
   let rec up_to x =
     if x > depth 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)
       | Proved (s, (_orlist, _cache)) -> 
@@ -1380,6 +1390,11 @@ let group_by_tac eq_predicate tactic status =
        with Not_found -> aux ([g] :: classes) tl
   in
   let classes = aux [] goals in
+  List.iter 
+   (fun 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
     List.map (fun x -> List.assoc x l2) l1