aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Mod_params.v
blob: 5151616601ad4bafdf28592b438d1a3bfafc4195 (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
38
39
40
41
42
43
44
45
46
47
48
49
50
(* Syntax test - all possible kinds of module parameters *)

Module Type SIG.
End SIG.

Module Type FSIG (X: SIG).
End FSIG.

Module F (X: SIG).
End F.

Module Q.
End Q.

(*
#trace Nametab.push;;
#trace Nametab.push_short_name;;
#trace Nametab.freeze;;
#trace Nametab.unfreeze;;
#trace Nametab.exists_cci;;
*)

Module M01. End M01.
Module M02 (X: SIG). End M02.
Module M03 (X Y: SIG). End M03.
Module M04 (X: SIG) (Y: SIG). End M04.
Module M05 (X Y: SIG) (Z1 Z: SIG). End M05.
Module M06 (X: SIG) (Y: SIG). End M06.
Module M07 (X Y: SIG) (Z1 Z: SIG). End M07.
Module M08 : SIG. End M08.
Module M09 (X: SIG) : SIG. End M09.
Module M10 (X Y: SIG) : SIG. End M10.
Module M11 (X: SIG) (Y: SIG) : SIG. End M11.
Module M12 (X Y: SIG) (Z1 Z: SIG) : SIG. End M12.
Module M13 (X: SIG) (Y: SIG) : SIG. End M13.
Module M14 (X Y: SIG) (Z1 Z: SIG) : SIG. End M14.
Module M15 := F Q.
Module M16 (X: FSIG) := X Q.
Module M17 (X Y: FSIG) := X Q.
Module M18 (X: FSIG) (Y: SIG) := X Y.
Module M19 (X Y: FSIG) (Z1 Z: SIG) := X Z.
Module M20 (X: FSIG) (Y: SIG) := X Y.
Module M21 (X Y: FSIG) (Z1 Z: SIG) := X Z.
Module M22 : SIG := F Q.
Module M23 (X: FSIG) : SIG := X Q.
Module M24 (X Y: FSIG) : SIG := X Q.
Module M25 (X: FSIG) (Y: SIG) : SIG := X Y.
Module M26 (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z.
Module M27 (X: FSIG) (Y: SIG) : SIG := X Y.
Module M28 (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z.