The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 27/09/2013 19:22, Abhishek Anand wrote:
> In the --ideslave mode, how to I tell coqtop to abort the current
> computation and ignore the last command?
> For example, if I  send repeat(simpl). , I wish there was a way to tell
> coqtop to abort and ignore last command ?
> Currently, I can restart coqtop and resend the contents of the
> file(except the last command), but for large files, it would waste a lot
> of time.

CoqIDE does this by sending coqtop a SIGINT signal. Indeed, Coq is
written to handle SIGINTs as interrupting the current computation. There
is a hack to support this under Windows, but that should basically do
the trick.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature