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
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
|
Module Type T. Parameter Inline(50) t : Type. End T.
Module Type F (X : T). Parameter p : X.t. End F.
Module M. Definition t := nat. End M.
Set Inline Level 49.
Module G
(X : F M [inline at level 49])
(Y : F M [inline at level 50])
(Z : F M) : F M [inline at level 50].
(* M.t should not be inlined in the type of X.p, because 49 < 50 *)
Goal X.p = X.p.
match goal with |- _ = _ :> M.t => idtac | _ => fail end.
Fail match goal with |- _ = _ :> nat => idtac | _ => fail end.
Abort.
(* M.t should be inlined in the type of Y.p, because 50 >= 50 *)
Goal Y.p = Y.p.
Fail match goal with |- _ = _ :> M.t => idtac | _ => fail end.
match goal with |- _ = _ :> nat => idtac | _ => fail end.
Abort.
(* M.t should not be inlined in the type of Z.p, because default level < 50 *)
Goal Z.p = Z.p.
match goal with |- _ = _ :> M.t => idtac | _ => fail end.
Fail match goal with |- _ = _ :> nat => idtac | _ => fail end.
Abort.
Definition p := X.p.
End G.
Module N. Definition p := 0. End N.
Module P := G N N N.
(* M.t should be inlined in the type of P.p, because 50 >= 50 *)
Goal P.p = P.p.
Fail match goal with |- _ = _ :> M.t => idtac | _ => fail end.
match goal with |- _ = _ :> nat => idtac | _ => fail end.
Abort.
Set Inline Level 50.
Module G'
(X : F M [inline at level 49])
(Y : F M [inline at level 50])
(Z : F M) : F M [inline at level 49].
(* M.t should be inlined in the type of Z.p, because default level >= 50 *)
Goal Z.p = Z.p.
Fail match goal with |- _ = _ :> M.t => idtac | _ => fail end.
match goal with |- _ = _ :> nat => idtac | _ => fail end.
Abort.
Definition p := X.p.
End G'.
Module P' := G' N N N.
(* M.t should not be inlined in the type of P'.p, because 49 < 50 *)
Goal P'.p = P'.p.
match goal with |- _ = _ :> M.t => idtac | _ => fail end.
Fail match goal with |- _ = _ :> nat => idtac | _ => fail end.
Abort.
Set Inline Level 50.
Module G''
(X : F M [inline at level 49])
(Y : F M [inline at level 50])
(Z : F M) : F M.
Definition p := X.p.
End G''.
Module P'' := G'' N N N.
(* M.t should not be inlined in the type of P''.p, because default level >= 50 *)
Goal P''.p = P''.p.
Fail match goal with |- _ = _ :> M.t => idtac | _ => fail end.
match goal with |- _ = _ :> nat => idtac | _ => fail end.
Abort.
Set Inline Level 49.
Module G'''
(X : F M [inline at level 49])
(Y : F M [inline at level 50])
(Z : F M) : F M.
Definition p := X.p.
End G'''.
Module P''' := G''' N N N.
(* M.t should not be inlined in the type of P'.p, because default level < 50 *)
Goal P'''.p = P'''.p.
match goal with |- _ = _ :> M.t => idtac | _ => fail end.
Fail match goal with |- _ = _ :> nat => idtac | _ => fail end.
Abort.
|
