The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

I just noticed the following behavior: when using asynchronous proof 
processing, as in Coqide, a goal that ends in Abort won't fully 
process.  As with:

Goal True.
idtac. (*or any one tactic that doesn't fail*)
fail. (*or any sequence of tactics that fails*)
Abort.

Instead of the above goal failing, asynchronous processing mode skips 
from the first tactic (idtac in this case - which is evaluated) directly 
to the Abort, seeming to ignore everything in between (it's left colored 
blue in Coqide, instead of green).  No failure occurs.

I don't know if this is the desired behavior of Abort under asynchronous 
processing mode, but some users might not anticipate such skipping, and 
might be using Abort-ending goals as tests.

-- Jonathan