The Coq mailing list

[Eric Tanter <etanter AT dcc.uchile.cl>]

On Dec 25, 2010, at 11:59 PM, Eric Tanter wrote:

> Note that I've just realized that the HTML page for Basics.v in SF:
> http://www.cis.upenn.edu/~bcpierce/sf/Basics.html
> 
> defines plus within a Playground2 module in order to not mess up with the 
> actual definition. 
> 
> But the file Basics.v that is distributed does not include these module 
> declarations, so the definition of plus given there does interfere. 

I now realize this has been fixed already online. I was using an older 
version of the files :/

> At this point, I guess I'm interested in understanding why the definition 
> of plus used in the code below does not work.

This is still the case!

Thanks,

-- Éric