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")
(require 'proof-site)
(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

Reply via email to