Questions tagged [proof-general]

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

3 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
1
vote
0answers
11 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-...
1
vote
0answers
64 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
0answers
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 ...