The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

Hello.

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

Anyway, here follows:

Inductive one : Prop := True.


Inductive two : Prop := True.

You won't be able to evaluate the second definition, Coq gives

Error: True already exists.

Sure, you could say that I shouldn't use Inductive in such cases, but still... (I noticed while using this 'Inductive' as a placeholder)

--
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.