% A parameterized module with a nested parameterized Inner module.
% The parent imports Inner at its own parameter and exports its items.
Module Nested[T].
Type p T -> prop.
Module Inner[U].
Kind inner type.
Type mk U -> inner.
Type q U -> prop.
End Inner.
Import Module I = Inner[T].
End Nested.
