+*)
+
+let prunable menv subst ty todo =
+ let rec aux = function
+ | (S(_,k,_,_))::tl ->
+ (match Equality.meta_convertibility_subst k ty menv with
+ | None -> aux tl
+ | Some variant -> no_progress variant tl (* || aux tl)*) )
+ | (D (_,_,T))::tl -> aux tl
+ | _ -> false
+ and no_progress variant = function
+ | [] -> prerr_endline "++++++++++++++++++++++++ no_progress"; true
+ | D ((n,_,P) as g)::tl ->
+ (match calculate_goal_ty g subst menv with
+ | None -> no_progress subst tl
+ | Some (_, gty) ->
+ (match calculate_goal_ty g variant menv with
+ | None -> assert false
+ | Some (_, gty') ->
+ if gty = gty' then
+ no_progress variant tl
+ else false))
+ | _::tl -> no_progress subst tl
+ in
+ aux todo
+
+;;