| (D (_,_,T))::tl -> aux tl
| _ -> false
and no_progress variant = function
| (D (_,_,T))::tl -> aux tl
| _ -> false
and no_progress variant = function
| D ((n,_,P) as g)::tl ->
(match calculate_goal_ty g subst menv with
| None -> no_progress variant tl
| D ((n,_,P) as g)::tl ->
(match calculate_goal_ty g subst menv with
| None -> no_progress variant tl
(debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize));
aux tables maxm flags cache orlist)
else if prunable_for_size flags s m todo then
(debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize));
aux tables maxm flags cache orlist)
else if prunable_for_size flags s m todo then
in
match auto_main tables newmeta context flags universe cache [elem] with
| Proved (metasenv,subst,_, tables,cache,_) ->
in
match auto_main tables newmeta context flags universe cache [elem] with
| Proved (metasenv,subst,_, tables,cache,_) ->