From c8d73368c6279460b6525834895ee2d65be3bda3 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 20 Oct 2011 15:54:22 +0000 Subject: [PATCH] We order alternatives according to the number of subgoals they open. --- matitaB/components/ng_tactics/nnAuto.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 -- 2.39.2