Questions tagged [proof-general]
Proof General is a generic front-end to several proof assistants such as Coq
8
questions
1
vote
0
answers
15
views
How to make the response-mode wrap text in proof general
I'm using proof general and I would like to have the response window wrap text. The default display is a three-window mode. The buffers are called proof-script-buffer proof-goals-buffer and proof-...
- 111
0
votes
0
answers
16
views
Proof general: Symbol’s value as variable is void: coq-prog-args
I'm trying to proof-assert-next-command-interactive, but get the following error in *Messages*:
proof-activate-scripting: Symbol’s value as variable is void: coq-prog-args.
I haven't found an ...
2
votes
1
answer
249
views
How to activate Coq for Org source blocks?
I have been writing some Coq code in Org, but when I try to run a source block, I get the following message:
No org-babel-execute function for coq!
I have tried to initialize the coq language in the ...
- 123
1
vote
0
answers
68
views
SSreflect not working with Emacs, Coq and ProofGeneral. How to install SSreflect in MacOS?
If I do something like - From mathcomp Require Import ssreflect. it gives me the following error.
Error: Cannot load mathcomp.ssreflect.ssreflect: no physical path bound to
mathcomp.ssreflect
But if ...
0
votes
1
answer
78
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 ...
- 121
1
vote
1
answer
129
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 (...
- 121
4
votes
1
answer
2k
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:
;...
- 151
2
votes
1
answer
134
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 ...
- 123