-(*
- let og_no = openg_no status in
- if (* og_no > flags.maxwidth || *)
- ((depth + 1) = flags.maxdepth && og_no <> 0) then
- (debug_print ~depth (lazy "pruned immediately"); None)
- else *)
- (* useless
- let status, cict = disambiguate status ctx ("",0,t) None in
- let status,ct = term_of_cic_term status cict ctx in
- let _,_,metasenv,subst,_ = status#obj in
- let ty = NCicTypeChecker.typeof subst metasenv ctx ct in
- let res = branch status (mk_cic_term ctx ty) in
- if smart=1 && og_no > res then
- (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = "
+ (* we compare the expected branching with the actual one and
+ prune the candidate when the latter is larger. The optimization
+ is meant to rule out stange applications of flexible terms,
+ such as the application of eq_f that always succeeds.
+ There is some gain but less than expected *)
+ let og_no = List.length (open_goals (depth+1) status) in
+ let status, cict = disambiguate status ctx ("",0,t) None in
+ let status,ct = term_of_cic_term status cict ctx in
+ let _,_,metasenv,subst,_ = status#obj in
+ let ty = NCicTypeChecker.typeof status subst metasenv ctx ct in
+ let res = branch status (mk_cic_term ctx ty) in
+ let diff = og_no - old_og_no in
+ debug_print (lazy ("expected branching: " ^ (string_of_int res)));
+ debug_print (lazy ("actual: branching" ^ (string_of_int diff)));
+ (* one goal is closed by the application *)
+ if og_no - old_og_no >= res then
+ (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = "