In case of error, capture if there is no goals and succeed instead

[spolu]

This does not solve the issue described here: https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F.20tactics/topic/delayed_abstraction.20meta-variables/near/242328447

But this is a step toward it with better error messages and a cleaner structure. Merging.