coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] New Coq version not seen by Proof General?

From: Clément Pit-Claudel <cpitclaudel AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] New Coq version not seen by Proof General?
Date: Sat, 28 Oct 2017 11:29:54 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=cpitclaudel AT gmail.com; spf=Pass smtp.mailfrom=cpitclaudel AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f179.google.com
Ironport-phdr: 9a23:6gTnrRBWjf3BO6QNtr8UUyQJP3N1i/DPJgcQr6AfoPdwSP39o8bcNUDSrc9gkEXOFd2Crakb26yL6+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6i760TlHERLmcAFxO+7dG4jIjs3x2frh1YfUZlBjgLu4bLVuGy23sUD6ssALjYZmYvI60hrVqX9BZuhbwUtnIFuSm1D34cLmr80ryDhZp/90r50Iaq79ZaltFbE=

On 2017-10-28 02:07, Chris Brinkley wrote:
> 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.

Super. Then setting coq-compiler to the corresponding value (with coqc
instead of coqtop) should do.

Clément.

[Coq-Club] New Coq version not seen by Proof General?, Chris Brinkley, 10/28/2017
- Re: [Coq-Club] New Coq version not seen by Proof General?, Clément Pit-Claudel, 10/28/2017
  - RE: [Coq-Club] New Coq version not seen by Proof General?, Chris Brinkley, 10/28/2017
    - Re: [Coq-Club] New Coq version not seen by Proof General?, Gaëtan Gilbert, 10/28/2017
      - Re: [Coq-Club] New Coq version not seen by Proof General?, Théo Zimmermann, 10/28/2017
    - Re: [Coq-Club] New Coq version not seen by Proof General?, Clément Pit-Claudel, 10/28/2017
- Re: [Coq-Club] New Coq version not seen by Proof General?, Ralf Jung, 10/28/2017
- <Possible follow-up(s)>
- Re: [Coq-Club] New Coq version not seen by Proof General?, Chris Brinkley, 10/28/2017