1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
(* When doing Module Foo with Definition bar := ..., bar must be
generated with the same polymorphism as Foo.bar. *)
Module Mono.
Unset Universe Polymorphism.
Module Type T.
Parameter foo : Type.
End T.
Module Type F(A:T). End F.
Set Universe Polymorphism.
Module M : T with Definition foo := Type.
Monomorphic Definition foo := Type.
End M.
End Mono.
Module Poly.
Set Universe Polymorphism.
Module Type T.
Parameter foo@{i|Set < i} : Type@{i}.
End T.
Module Type F(A:T). End F.
Unset Universe Polymorphism.
Module M : T with Definition foo := Set : Type.
Polymorphic Definition foo := Set : Type.
End M.
End Poly.
|
