The Coq mailing list

["Carlos.SIMPSON" <carlos AT math1.unice.fr>]

Hi. Does anybody have any comments on the following behavior?  Is it a
problem which will
be fixed in a future release?

---Carlos Simpson

Parameter A : Type.

Parameter f : A -> A.

Module Type Mm.
Parameter a : A.
End Mm.

Module Constr [U:Mm] : Mm.
Definition a := (f U.a).

End Constr.


Module Constr2 [V:Mm].
Module Z := (Constr V).
Module Z2 := Z.
Module Z3 := (Constr V).

Lemma lem1 : Z.a == Z2.a.
Reflexivity.
Save.

Lemma lem2 : Z.a == Z3.a.
Reflexivity.

Toplevel input, characters 0-11
> Reflexivity.
> ^^^^^^^^^^^
Error: Impossible to unify Z3.a with Z.a