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
(* 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
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)));