The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
-------- Forwarded Message --------
Subject: Using Proof-General with the HoTT Modification to Coq
Date: Wed, 22 Apr 2015 17:38:17 -0700
From: Casey Coleman <colem...@mail.chapman.edu>
I am trying to use PG with a modified version of Coq suitable for
Homotopy Type Theory. Here's the project's GitHub page:
The recommended course of action is to set proof-prog-name-ask to "t" in
the ~/.emacs file. This doesn't have any effect.
I tried the following, which broke PG until I removed it:
(add-to-list 'load-path "/path/to/proof-general/generic")
(setq proof-prog-name-ask t)
(setq coq-prog-args '("-emacs"))
(setq coq-prog-name "/path/to/hoqtop")
where the paths are substituted for their actual values.
I'm using the latest version of PG in Ubuntu 14. I know that hoqtop
works (it is essentially coqtop with some modifications). How can I get
PG to work with hoqtop?
ProofGeneral mailing list