Open
Description
Q.PAT_X_ASSUM (aka qpat_x_assum) returns bad error messages because its implementation can't distinguish between an expected failure (the pattern not matching an unrelated assumption) and an unexpected failure (the continuation failing). Sometimes this is inevitable because there may be multiple parses for the pattern, but if there's only one, the error could be better. (Incidentally, the behaviour probably shouldn't be to try to find the first assumption that both matches the pattern and has the continuation succeed.)
Prompted by some discussion on Discord .