coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proof generals, coqdep and 8.5

From: "John Wiegley" <johnw AT newartisans.com>
To: Yannick <yannick.zakowski AT irisa.fr>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Proof generals, coqdep and 8.5
Date: Wed, 28 Oct 2015 09:54:07 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-pa0-f53.google.com
Ironport-phdr: 9a23:bFGEqRX+G6gs4w6YuQf3EHSP89fV8LGtZVwlr6E/grcLSJyIuqrYZhGAt8tkgFKBZ4jH8fUM07OQ6PC9HzVeqsja+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8CVOlsD2mH1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GI1RCjInOGN9sNzisx/CRgjJ9HIfVXoNkRtgAhLE9xi8UI2n4QXgse8okgudPcu+crE5VjCv/u0jHB3viCEYHzg072jNls1rhaRA5hmmokoskMbvfIiJOa8mLevmdtQASD8ZUw==
Organization: New Artisans LLC

>>>>> Yannick
>>>>> <yannick.zakowski AT irisa.fr>
>>>>> writes:

> Hence the question: am I missing something or was the change partial and is
> Proof General currently incompatible with Coq 8.5b2?

I use Proof General 4.3prexxx with Coq 8.5b2. I only use the -R flag, like
this in my _CoqProject file:

-R Hask/src Hask -R src LinearScan

John

[Coq-Club] Proof generals, coqdep and 8.5, Yannick, 10/28/2015
- Re: [Coq-Club] Proof generals, coqdep and 8.5, John Wiegley, 10/28/2015
- Re: [Coq-Club] Proof generals, coqdep and 8.5, Pierre Courtieu, 10/29/2015
  - Re: [Coq-Club] Proof generals, coqdep and 8.5, Yannick, 10/29/2015