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: Fri, 27 Oct 2017 23:40:56 -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-qt0-f171.google.com
Ironport-phdr: 9a23:5aZV7Bd+lyVpoyOeWtNUOW9VlGMj4u6mDksu8pMizoh2WeGdxc28YB7h7PlgxGXEQZ/co6odzbGJ4+a9ASQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpW1aJhKqPg1sY+/xB4T6jsKt1un09YeATR9PgW+WZTJ3IROqmj3Qqow9hYJ/Jqs1gk/CunpUcOBf2G9lIXqcmh/94oG7+5s1oHcYgO4o68MVCfayRK8/V7ENVDk=

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.

You can customize coq-prog-name; alternatively, make sure that running coqtop
in your shell runs the right version of Coq.

[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