forked from coq/coq
-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathHintLocality.v
102 lines (67 loc) · 1.99 KB
/
HintLocality.v
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
102
(** 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.
#[global] Hint Cut [ _ ] : secdb.
#[global] Hint Mode S ! : secdb.
#[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.
(** Variant of the above test
- modes are correctly generalized at section closure
- non-local section-specific hints trigger a warning
*)
Create HintDb seclocaldb.
Set Warnings "non-local-section-hint".
Section SecLocal.
Variable A : Type.
Definition refl (n : A) : n = n := eq_refl.
Variable prf : forall n : nat, n = 0.
#[export] Hint Mode refl ! : seclocaldb.
#[export] Hint Mode prf ! : seclocaldb.
#[export] Hint Cut [ prf ] : seclocaldb.
#[export] Hint Variables Transparent : seclocaldb.
#[export] Hint Constants Transparent : seclocaldb.
#[export] Hint Opaque prf : seclocaldb.
End SecLocal.
Print HintDb seclocaldb.