The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

ohh, I get it now, lol

My confusion was due to the fact that I meant True as the one in Prop, and not a constructor element :x

2013/8/2 Adam Chlipala <adamc AT csail.mit.edu>

It doesn't look like a bug to me.  Coq uniformly enforces a rule that a given "global" identifier may only be defined once per scope (e.g., module) that permits "global" identifier definitions.

On 08/02/2013 12:03 PM, Nuno Gaspar wrote:

I believe this is a bug, but then again probably it would have been noticed by now..

Inductive one : Prop := True.


Inductive two : Prop := True.

You won't be able to evaluate the second definition.

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.