Proof general configuration for the Coq Software Foundations tutorial18 May 2015, by Artur Malabarba.
Proof-general is a powerful client for the Coq proof assistant, and Software Foundations is great interactive tutorial for the language. As I was following the tutorial, I felt the need to speed things up a little bit. Today’s post is just some configuration code I wrote for that effect.
Parts of it might be useful for coq in general, but its mostly optimized to minimize keystrokes in the tutorial, and sometimes it leaves bad indentation or extra lines all over the place.
These are some common abbrevs, and an advice so you don’t have to hit SPC before M-n.
And finally, the most important snippet. Just make sure you install
company-coq from Melpa.