currently, proof-shell-filter looks for urgent messages before
looking for errors. Moreover, if an urgent message is found, it
searches for errors only in the output that follows the urgent
This behavior is responsible for issue #463, where Coq outputs an
error before a warning and the error is lost because the warning
is recognized as urgent message.
What is the problem here? Coq outputting the warning _after_ the
error? Or matching the warning as urgent message? Or searching
for errors only behind urgent messages?
ProofGeneral-devel mailing list