lean#476 conv mode find and for

Stream: PR reviews

[Eric Wieser]

The find and for tactics in conv mode (and therefore also conv in ... {}) all throw away error messages, which is a very frustrating experience for me.

I've a fix at lean#476, I'd greatly appreciate if someone could review

[Eric Wieser]

There was some previous discussion about the PR in https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F.20tactics/topic/instances.20for.20meta.20defs/near/212738421