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
0 answers
17 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
1 vote
0 answers
72 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
0 answers
20 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