blob: dcfcc98d5829a26dbd43f483aaa58a2be6de6c81 (
plain)
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
32
33
34
35
36
37
|
Module Type TA.
Parameter t : Set.
End TA.
Module Type TB.
Declare Module A: TA.
End TB.
Module Type TC.
Declare Module B : TB.
End TC.
Module Type TD.
Declare Module B: TB .
Declare Module C: TC
with Module B := B .
End TD.
Module Type TE.
Declare Module D : TD.
End TE.
Module Type TF.
Declare Module E: TE.
End TF.
Module G (D: TD).
Module B' := D.C.B.
End G.
Module H (F: TF).
Module I := G(F.E.D).
End H.
Declare Module F: TF.
Module K := H(F).
|
