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 unnecessa

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/ http://coqpide.bitbucket.org/ ) but there's also an Eclipse system built on it too ( https://coqoon.github.io/cav2015/ https://coqoon.github.io/cav2015/ )