2007-12-04.txt:16:34:26: <faxathisia> You can use Proof General mode in emacs
2007-12-04.txt:16:34:45: <faxathisia> anyway Proof General seems good
2010-07-25.txt:16:02:26: <aliseiphone> Phantom_Hoover: My Coq recommendation: Use Emacs with Proof General. Three window mode and electric mode.
2010-08-21.txt:00:24:22: <botte> coq's syntax is better than agda for people who actually use it. interactive development is possible with Proof General; much nicer than Agda's mode. Proving things in Agda is almost impossible; it is not developed for that at all, while Coq is built around it. ProofGeneral makes it even nicer.
2010-12-11.txt:23:26:00: <elliott> Proof General is godly.
2010-12-11.txt:23:26:21: <elliott> "# See the Proof General Eclipse wiki for screenshots of Proof General in Eclipse."
2010-12-11.txt:23:40:32: <elliott> Phantom_Hoover: BTW, Proof General can list all the tactics in the system (there's fewer than you think).
2011-08-05.txt:10:56:07: <elliott> coppro: Umm, Coq is used via Proof General (nicer) or coqtop (interactive command-line system).
2011-08-05.txt:10:57:37: <elliott> Proof General -- built on top of Emacs -- is by far the nicest way to use Coq.
2011-08-05.txt:11:00:53: <elliott> Phantom_Hoover: Proof General uses that, right?
2011-11-16.txt:20:20:31: <Phantom__Hoover> <elliott> http://i.imgur.com/1uOhf.png ;; this is the first time I have ever used three windows in Emacs ← You've never used Proof General?
2012-04-30.txt:23:12:43: <elliott> Proof General is really, really nice (with a few config tweaks).
2012-04-30.txt:23:12:56: <elliott> shachaf: Because of Proof General.