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
103
104
105
106
107
108
|
(** Testing the Typeclasses Opaque hints. We create two identical typeclasses [P] and [Q] and compare the behaviour of Typeclasses Opaque and Hint Opaque. They should be the same. *)
Axiom A : Type.
Axiom P : A -> Type.
Axiom Q : A -> Type.
Existing Class P.
Existing Class Q.
Axiom a : A.
Axiom pa : P a.
Axiom qa : Q a.
#[local] Existing Instance pa.
#[local] Existing Instance qa.
Definition b := a.
Definition c := a.
(** b is transparent so typeclass search should find it. *)
Goal P b.
Proof.
Succeed typeclasses eauto.
Abort.
(** c is transparent so typeclass search should find it. *)
Goal Q c.
Proof.
Succeed typeclasses eauto.
Abort.
(** Creating a local hint in a module or a section *)
Section Foo.
#[local] Hint Opaque b : typeclass_instances.
#[local] Typeclasses Opaque c.
End Foo.
(** Closing the module/section should get rid of the hint, so we expect the same behaviour as before. *)
(** b is transparent so typeclass search should find it. *)
Goal P b.
Proof.
Succeed typeclasses eauto.
Abort.
(** c is transparent so typeclass search should find it. *)
Goal Q c.
Proof.
Succeed typeclasses eauto.
Abort.
(** Now setting the locality as export *)
Module Foo.
#[export] Hint Opaque b : typeclass_instances.
#[export] Typeclasses Opaque c.
(** Things should fail inside *)
Goal P b.
Proof.
Fail typeclasses eauto.
Abort.
Goal Q c.
Proof.
Fail typeclasses eauto.
Abort.
End Foo.
(** But succeed outside *)
Goal P b.
Proof.
Succeed typeclasses eauto.
Abort.
Goal Q c.
Proof.
Succeed typeclasses eauto.
Abort.
(** Until of course we export the module *)
Export Foo.
Goal P b.
Proof.
Fail typeclasses eauto.
Abort.
Goal Q c.
Proof.
Fail typeclasses eauto.
Abort.
(** Finally we test the localities for this alias *)
Succeed #[local] Typeclasses Opaque b.
Succeed #[global] Typeclasses Opaque b.
Succeed #[export] Typeclasses Opaque b.
Succeed #[local] Typeclasses Transparent b.
Succeed #[global] Typeclasses Transparent b.
Succeed #[export] Typeclasses Transparent b.
Notation bar := (0 + 0).
Fail Local Typeclasses Transparent bar.
Notation baz := b.
Succeed Local Typeclasses Transparent baz.
|
