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. see: http://proofgeneral.inf.ed.ac.uk/htmlshow.php?title=Proof+General+adapting+manual&file=releases%2FProofGeneral%2Fdoc%2FPG-adapting%2FPG-adapting_15.html#index-proof_002dshell_002dfilter _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.