aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Mod_params.v
blob: 74228bbbfaf042ab037cefe9d8c570ad3d0178fe (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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
(* 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 M.
Reset M.
Module M (X: SIG).
Reset M.
Module M (X Y: SIG).
Reset M.
Module M (X: SIG) (Y: SIG).
Reset M.
Module M (X Y: SIG) (Z1 Z: SIG).
Reset M.
Module M (X: SIG) (Y: SIG).
Reset M.
Module M (X Y: SIG) (Z1 Z: SIG).
Reset M.
Module M : SIG.
Reset M.
Module M (X: SIG) : SIG.
Reset M.
Module M (X Y: SIG) : SIG.
Reset M.
Module M (X: SIG) (Y: SIG) : SIG.
Reset M.
Module M (X Y: SIG) (Z1 Z: SIG) : SIG.
Reset M.
Module M (X: SIG) (Y: SIG) : SIG.
Reset M.
Module M (X Y: SIG) (Z1 Z: SIG) : SIG.
Reset M.
Module M := F Q.
Reset M.
Module M (X: FSIG) := X Q.
Reset M.
Module M (X Y: FSIG) := X Q.
Reset M.
Module M (X: FSIG) (Y: SIG) := X Y.
Reset M.
Module M (X Y: FSIG) (Z1 Z: SIG) := X Z.
Reset M.
Module M (X: FSIG) (Y: SIG) := X Y.
Reset M.
Module M (X Y: FSIG) (Z1 Z: SIG) := X Z.
Reset M.
Module M : SIG := F Q.
Reset M.
Module M (X: FSIG) : SIG := X Q.
Reset M.
Module M (X Y: FSIG) : SIG := X Q.
Reset M.
Module M (X: FSIG) (Y: SIG) : SIG := X Y.
Reset M.
Module M (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z.
Reset M.
Module M (X: FSIG) (Y: SIG) : SIG := X Y.
Reset M.
Module M (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z.
Reset M.