coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] bug or feature

From: Adam Chlipala <adamc AT csail.mit.edu>
To: Nuno Gaspar <nmpgaspar AT gmail.com>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] bug or feature
Date: Fri, 02 Aug 2013 12:05:33 -0400

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.

[Coq-Club] bug or feature, Nuno Gaspar, 08/02/2013
- Re: [Coq-Club] bug or feature, Adam Chlipala, 08/02/2013
  - Re: [Coq-Club] bug or feature, Nuno Gaspar, 08/02/2013
    - Re: [Coq-Club] bug or feature, Kristopher Micinski, 08/02/2013