goal_tac: finish marked assumptions from left to right -- corresponds better with the strategy of etac, with significant performance gains in some situations;

eq_assumption: slightly more efficient by checking (open) result of Logic.assum_problems directly; tuned;