-- 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> Hello, I am trying to use PG with a modified version of Coq suitable for Homotopy Type Theory. Here's the project's GitHub page: https://github.com/HoTT/HoTT 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 ProofGeneral@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral
