The Coq mailing list

[Chris Brinkley <Chris.Brinkley AT sslmda.com>]

With apologies for tangential elementary question, how do I tell ProofGeneral to use a newer version of Coq or a different Coq directory than it was previously?   Could not find anything in ProofGeneral doc or general google search about this.  I’m sure there must be a way to do this, but what is it?

 

I just upgraded Software Foundations to 5.3, and immediately found at least one line that used a command unsupported in my previous Coq version.  (Command yields “Error: There is no option Warnings.”)  So, I used OPAM to install Coq 8.6 (8.7 package not available yet) alongside the existing earlier Coq version on my Ubuntu laptop.  Install process said something about setting default Coq version to 8.6. 

 

But now when I run the troublesome command from Software Foundations 5.3, I still get the same error, which makes me think ProofGeneral is not seeing the new Coq version.

 

---

This message (including any attachments) may contain confidential information intended for a specific individual and purpose. If you are not the intended recipient, you should delete this message and any attachments.