The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 19/09/2015 00:42, Bruno Le Floch wrote:
> As far as I can tell, the second example uses the same syntax as the
> first (just replacing one by two and two by three).  I might be
> missing something.

Yes. This oddity has been introduced by commit dac89096 dating back from
2003:

https://github.com/coq/coq/commit/dac8909686ba0c79e5fa35c9b04122b6f5f81e02

It looks like the syntax translator from V7 to V8 lost part of term
annotations. I am going to fix this.

Thanks for the report,
PMP

Attachment: signature.asc
Description: OpenPGP digital signature