- debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty));
- if is_subsumed depth status closegty (snd cache.under_inspection) then
+ debug_print ~depth (lazy("Attacking goal " ^
+ string_of_int g ^ " : "^ppterm status gty));
+ debug_print ~depth (lazy ("current failures: " ^
+ string_of_int (List.length (all_elements ctx cache.failures))));
+ let is_eq =
+ let _,_,metasenv,subst,_ = status#obj in
+ 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 -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)));
+ auto_main flags signature cache (depth+1) status)
+ (* check for loops *)
+ else if is_subsumed depth false status closegty (snd cache.under_inspection) then