Questions tagged [proof-general]

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

Filter by
Sorted by
Tagged with
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-...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
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 (...
user avatar
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: ;...
user avatar
  • 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 ...
user avatar
  • 123