The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Hello.

I have strange problem with modules.
I import module this way:

Require Import FileX.
Module Y (X : Module X).
Module Z := ModuleZ X.
Import Z.
...

But afteer that I have definitions from ModuleZ imported twice:
in plain Def form and in from ModuleZ.Def.
That causes some problems (auto-inferred types use un-qualified form
and therefore I need to manually write all types + type them in
qualified form).

What can cause such behaviour? Is there workaround?

Sincerely,
Kirill Taran