Coq module crap

crappymod.v

Module Type AT.
Parameter x : nat.
End AT.

Module A (Import a : AT).
Include a.
Definition y := a.x.

End A.
Print A.

Module AP : AT.
Definition x := 42.
End AP.


Module A' := A AP.
Print A'.
Print A'.y.
Print A'.x.


Module Type Aall (Import a : AT).
Include (A a).
End Aall.