Disabled debug.

[helm.git] / matita / components / ng_tactics / nnAuto.ml

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index cb42b56912118374391671152644550aba10eef3..72099fbd3ead131956f9ad0e1c142a389ef3c3c6 100644 (file)
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -905,7 +905,7 @@ let sort_candidates status ctx candidates =
   let candidates = 
      List.sort (fun (a,_) (b,_) -> a - b) candidates in 
   let candidates = List.map snd candidates in
-    noprint (lazy ("candidates =\n" ^ (String.concat "\n" 
+    debug_print (lazy ("candidates =\n" ^ (String.concat "\n" 
        (List.map (NotationPp.pp_term status) candidates))));
     candidates
 
@@ -1393,8 +1393,8 @@ let do_something signature flags status g depth gty cache =
   (* states in l1 have have an empty set of subgoals: no point to sort them *)
   debug_print ~depth 
     (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2)))));
-    (* l1 @ (sort_new_elems (l @ l2)), cache *)
-    l1 @ (List.rev l2) @ l, cache 
+    (* we order alternatives w.r.t the number of subgoals they open *)
+    l1 @ (sort_new_elems l2) @ l, cache 
 ;;
 
 let pp_goal = function