When goals are displayed by Isabelle in ProofGeneral, assumptions are rendered as having brackets around them as so: In Isabelle/jEdit, however, this seems to have changed to meta-implication ar...

I'm trying to use coq with ProofGeneral, but the built-in Verilog mode shadows *.v filetype recognition. Can I somehow disable it and let ProofGeneral remap them to its coq mode?

In most IDEs or text editors, you can right-click a term and it takes you to the file where that term is defined. CoqIDE doesn't seem to have that, so I've been doing coqdoc myfile.v --html, then g...

Probably a coq newbie question, but I could not find a ready solution so I'll ask here for reference. The cocq version is 8.5pl2 I tried to build coqfj. The first make attempt has failed with some...

Unlike Agda, Coq tends to separate proofs from functions. The tactics Coq gives are great for writing proofs, but I'm wondering if there is a way to replicate some Agda-mode functionality. Specifi...

I've been trying to learn to use Isabelle 2016. While in principle I like the idea of asynchronous proof checking, I don't like Isabelle/jEdit for a number of reasons, the most severe of which is t...

I'm using Proof General in Emacs on Aquamacs and every time I write a period (".") everything is executed (up to that period). It seems like an electric behavior but it's not. All other keys behave...

Edit 4: It turns out that this is actually just a limitation of TTY input in general; there's nothing specific about OCaml, Coq, or Emacs which is causing the problem. I'm working on a Coq program...

This question has to do with configuring the Coq mode within Proof General, in Emacs. I'm trying to have Emacs automatically replace keywords and notation in Coq with the corresponding Unicode gly...