[chriswarbo]

I see that it uses the 'traditional' stepping forwards/backwards like ProofGeneral and CoqIDE.

Improvements have been made in Coq 1.5 which make this unnecessary: using the PIDE system (originally from Isabelle) you can now throw the whole file at Coq, then send it diffs as the user makes edits. No need to rewind, go-to, etc.

I've used this in jEdit ( http://coqpide.bitbucket.org/ ) but there's also an Eclipse system built on it too ( https://coqoon.github.io/cav2015/ )

[chriswarbo]

Of course I meant 8.5, not 1.5!

[Ptival]

Thanks, this is very interesting and I'd love to switch to 8.5.

I might wait a little for my benchmarks to be 8.5 ready though!