X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=72099fbd3ead131956f9ad0e1c142a389ef3c3c6;hb=6114cb246d344e93b0dfeae4d273dc4422633ecb;hp=9ea4dc03df55518692f62dfdc7b7267f9fdba478;hpb=d29f657ab297eb0570f6036d7eb67582404962f2;p=helm.git

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 9ea4dc03d..72099fbd3 100644
--- 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
@@ -1668,7 +1668,7 @@ auto_main flags signature cache depth status: unit =
            NCicParamod.is_equation status metasenv subst ctx ty in
         (* if the goal is an equality we artificially raise its depth up to
            flags.maxdepth - 1 *)
-        if (not flags.last && is_eq && (depth < (flags.maxdepth -1))) then
+        if (not flags.last && is_eq && (depth < (flags.maxdepth -2))) then
         (* for efficiency reasons, in this case we severely cripple the
            search depth *)
           (debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1)));
@@ -1722,7 +1722,7 @@ auto_main flags signature cache depth status: unit =
               let dty = NCic.Appl [NCic.Implicit (`Typeof depth); ty] in
               mk_cic_term ctx dty 
             in 
-            prerr_endline ("FAILURE : " ^ ppterm status gty);
+            (*prerr_endline ("FAILURE : " ^ ppterm status gty);*)
             add_to_th newfail failures closegty
           else failures in
         debug_print ~depth (lazy "no more candidates");