coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq 8.6 change poll

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Coq 8.6 change poll
Date: Tue, 31 May 2016 11:27:47 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qg0-f41.google.com
Ironport-phdr: 9a23:JaYpxRwUorlqd0TXCy+O+j09IxM/srCxBDY+r6Qd0ekfIJqq85mqBkHD//Il1AaPBtWKra8ZwLqG+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuSt+U0pn8h7D60qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mosVHSODxe7kyZb1eFjUvdW4vt+PxshyWbwyJ72ccW2NethdJHQXD8FmuXJD3syj3sudw8CafNMzyC7szXGLxvO9QVBb0hXJfZHYC+2bNh5kogQ==

On 05/31/2016 11:05 AM, Pierre-Marie Pédrot wrote:

... Likewise, for reasons I am not really sure to understand, it
forces you to write the ugly

constr:((x, y))

when parsing pairs.

On closer inspection, I found one instance of "constr:(x, y)". But just one, no big deal.

An important question is - when 8.6 tries to parse a badly formed constr: such as "constr:(x, y)", what will the error message say?

-- Jonathan

[Coq-Club] Coq 8.6 change poll, Pierre-Marie Pédrot, 05/31/2016
- Re: [Coq-Club] Coq 8.6 change poll, Jonathan Leivent, 05/31/2016
  - Re: [Coq-Club] Coq 8.6 change poll, Pierre-Marie Pédrot, 05/31/2016
- Re: [Coq-Club] Coq 8.6 change poll, Jonathan Leivent, 05/31/2016
  - Re: [Coq-Club] Coq 8.6 change poll, Pierre-Marie Pédrot, 05/31/2016
  - Re: [Coq-Club] Coq 8.6 change poll, Jason Gross, 05/31/2016