The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

For autodetection of opam executables you may need to restart emacs for 
it to get the right PATH.

You can also look at variables coq-dependency-analyzer and coq-compiler.

Gaëtan Gilbert

On 28/10/2017 08:07, Chris Brinkley wrote:
> I tried adding (setq coq-prog-name "~/opam-coq.8.6/4.01.0/bin/coqtop") to 
> init.el.
>
> Emacs seems to accept the initialization and I no longer get the error executing 
> interactively, but I still get an error compiling a file containing a "Set 
> Warnings" command , which makes me doubt if ProofGeneral is using coqc 8.6, even 
> though it now seems to be using coqtop 8.6.
>
> Is there an analogous way to control the coqc version ProofGeneral will use?
>
> Clément Pit-Claudel wrote:
> > You can customize coq-prog-name; alternatively, make sure that running coqtop 
> > in your shell runs the right version of Coq.
>
> > On 2017-10-27 23:28, Chris Brinkley wrote:
> > > 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.