Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [proof-general]

Proof General is a generic front-end to several proof assistants such as Coq

0
votes
1answer
22 views

Why does Evil autocomplete simpl. ESC to beta delta [] iota zeta.?

This might be a strange question but every time I type: simpl. <ESC> Evil substitutes it with: simpl beta delta [] iota zeta. this is driving me nuts. Why is this happening and more ...
1
vote
1answer
27 views

How does one save and close a file in Proof General without all of Evil shutting down?

I am using evil (emacs+vim). I am also using Proof General for the theorem prover Coq. I was trying to work with emacs but whenever I do: :x or :q in my coq .v file all of emacs closes as well (...
4
votes
1answer
573 views

How to add symbols to prettify and pretty modes?

I am trying to configure Emacs with ProofGeneral (the Coq IDE) to display mathematical symbols in place of the abbreviations ->, =>, forall and exists. My current .emacs script is as follows: ;...
2
votes
1answer
98 views

proof-general no newline after C-c C-n

I am using proof-general mode for editing and executing Coq files in emacs. However, I am highly annoyed by the C-c C-n behavior of always going to the next line if the EoF is reached. As I tend to ...