blob: dce19318c5ac39c79d8b0f5e1e91d3e8b8d5331c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
Module Type T.
Polymorphic Parameter Inline t@{i} : Type@{i}.
End T.
Module M.
Polymorphic Definition t@{i} := nat.
End M.
Module Make (X:T).
Include X.
End Make.
Module P := Make M.
|