The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I don't know if anyone has responded to you, or if you resolved this, and sorry for the rather late reply, but this sounds like a bug you should report on the bug tracker, if the behavior still exists.

-Jason

On Aug 17, 2014 3:54 AM, "Jonathan" <jonikelee AT gmail.com> wrote:

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