From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 20 Oct 2011 15:54:22 +0000 (+0000)
Subject: We order alternatives according to the number of subgoals they open.
X-Git-Tag: make_still_working~2165
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=c8d73368c6279460b6525834895ee2d65be3bda3

We order alternatives according to the number of subgoals they open.
---

diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml
index d77fd2f74..8cf11d98c 100644
--- a/matitaB/components/ng_tactics/nnAuto.ml
+++ b/matitaB/components/ng_tactics/nnAuto.ml
@@ -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