From 223f026e4f5a9f273f88952b0548fea63b65afd1 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 20 Oct 2011 15:47:59 +0000 Subject: [PATCH] Alternatives are ordered according to the number of subgoals they generate. --- matita/components/ng_tactics/nnAuto.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml index cb42b5691..0b3cd9361 100644 --- a/matita/components/ng_tactics/nnAuto.ml +++ b/matita/components/ng_tactics/nnAuto.ml @@ -14,7 +14,7 @@ open Printf let print ?(depth=0) s = prerr_endline (String.make (2*depth) ' '^Lazy.force s) let noprint ?(depth=0) _ = () -let debug_print = noprint +let debug_print = print open Continuationals.Stack open NTacStatus @@ -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 -- 2.39.2