The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

> 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.

Which version of ProofGeneral are you using?  Most (all?) distros
package extremely outdated versions.  I recommend using the latest
version from GitHub: <https://github.com/ProofGeneral/PG>

Btw, Coq 8.7 is available in opam for 10 days now, ever since
<https://github.com/ocaml/opam-repository/pull/10493> got merged.

Kind regards,
Ralf