The Coq mailing list

[Robin Green <greenrd AT greenrd.org>]

On Tue, 13 Nov 2007 10:02:24 +0000
Edsko de Vries 
<devriese AT cs.tcd.ie>
 wrote:

> Sorry to reply to my own post, but I just found out that when I avoid
> calling the 'Module' and the coq file the same thing, the problem
> disappears. Not sure why though!

If I understand correctly, the file is also a module, but a different
kind of module (that's why you use Require Import to import files) - and
thus what you experienced was a namespace collision.
-- 
Robin