The Coq mailing list

[td202 AT doc.ic.ac.uk]

I am having an issue where a module (D) is importing two other modules (B and
C) which each import another module (A) that is common to both.  (The modules
in this case are all parameterised (functors).)  My problem is that Coq does
not identify B's copy of A with C's copy.

Here is some code that demonstrates my problem:
Module Type KO.
Parameter x : Type.
End KO.

Module A (Import ko : KO).
Inductive foo := zeb : x -> foo.
End A.

Module B (ko : KO).
Module Import X:=A ko.
Definition flob (f : foo) : foo := f.
End B.

Module C (ko : KO).
Module Import X:=A ko.
Definition flip (f : foo) : foo := f.
End C.

Module D (ko : KO).
Module Import MyB := B ko.
Module Import MyC := C ko.

Lemma flobflip : forall f, flob (flip f) = f.

The last line gives the following error:
Error: In environment
f : X.foo
The term "flip f" has type "X.foo" while it is expected to have type
 "MyB.X.foo".

Is there some way that I can get Coq to identify MyB.X and MyC.X?  If not, is
there a sensible workaround?  (I'm running version 8.3pl2.)

Thanks and regards
-- Thomas Dinsdale-Young