blob: 4481335907c481319be7ce88e97eb4817d74950c (
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
|
(** Test hint command locality w.r.t. modules *)
Create HintDb foodb.
Create HintDb bardb.
Create HintDb quxdb.
#[global] Hint Immediate O : foodb.
#[global] Hint Immediate O : bardb.
#[global] Hint Immediate O : quxdb.
Module Test.
#[global] Hint Cut [ _ ] : foodb.
#[global] Hint Mode S ! : foodb.
#[global] Hint Opaque id : foodb.
#[global] Remove Hints O : foodb.
#[local] Hint Cut [ _ ] : bardb.
#[local] Hint Mode S ! : bardb.
#[local] Hint Opaque id : bardb.
#[local] Remove Hints O : bardb.
#[export] Hint Cut [ _ ] : quxdb.
#[export] Hint Mode S ! : quxdb.
#[export] Hint Opaque id : quxdb.
#[export] Remove Hints O : quxdb.
(** All three agree here *)
Print HintDb foodb.
Print HintDb bardb.
Print HintDb quxdb.
End Test.
(** bardb and quxdb agree here *)
Print HintDb foodb.
Print HintDb bardb.
Print HintDb quxdb.
Import Test.
(** foodb and quxdb agree here *)
Print HintDb foodb.
Print HintDb bardb.
Print HintDb quxdb.
(** Test hint command locality w.r.t. sections *)
Create HintDb secdb.
#[global] Hint Immediate O : secdb.
Section Sec.
Fail #[global] Hint Cut [ _ ] : secdb.
Fail #[global] Hint Mode S ! : secdb.
Fail #[global] Hint Opaque id : secdb.
Fail #[global] Remove Hints O : secdb.
#[local] Hint Cut [ _ ] : secdb.
#[local] Hint Mode S ! : secdb.
#[local] Hint Opaque id : secdb.
#[local] Remove Hints O : secdb.
Print HintDb secdb.
End Sec.
Print HintDb secdb.
|
