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?

From Proof General's point of view, the first of these is the problem, since the behaviour has been well specified for a long time and I guess that Coq's behaviour has changed over time. See fragment of documentation from proof-shell-filter below.

 - David

Error or interrupt messages are expected to terminate an
interactive output and appear last before a prompt and will
always be processed.  Error messages and interrupt messages are
therefore *not* considered as urgent messages.


ProofGeneral-devel mailing list

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to