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
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
|
(** This file tests how locality attributes affect usual vernacular commands.
PLEASE, when this file fails to compute following a voluntary change in
Coq's behaviour, modify accordingly the tables in [sections.rst] and
[modules.rst] in [doc/sphinx/language/core]
Also look at the corresponding discussions about locality attributes in the
refman (directory doc/sphinx)
- For Definition, Lemma, ..., look at language/core/definitions.rst
- For Axiom, Conjecture, ..., look at language/core/assumptions.rst
- For abbreviations, look at user-extensions/syntax-extensions.rst
- For Notations, look at user-extensions/syntax-extensions.rst
- For Tactic Notations, look at user-extensions/syntax-extensions.rst
- For Ltac, look at proof-engine/ltac.rst
- For Canonical Structures, look at language/extensions/canonical.rst
- For Hints, look at proofs/automatic-tactics/auto.rst
- For Coercions, look at addendum/implicit-coercions.rst
- For Ltac2, look at proof-engine/ltac2.rst
- For Ltac2 Notations, look at proof-engine/ltac2.rst
- For Set, look at language/core/basic.rst
*)
From Ltac2 Require Import Ltac2.
(** ** Tests for modules and visibility attributes with Ltac2 *)
(* A parameter: *)
Parameter (secret : nat).
(* An axiom: *)
Axiom secret_is_42 : secret = 42.
(** *** Without attribute (default) *)
Module InModuleDefault.
Module Bar.
(* A custom tactic: *)
Ltac2 find_secret () := rewrite secret_is_42.
Ltac2 Notation "rfl" := reflexivity.
End Bar.
(** **** Without importing: *)
(* Availability of the tactic *)
Fail Print find_secret.
Print Bar.find_secret.
(* Availability of the tactic notation *)
Lemma plop_ni : 2 + 2 = 4.
Proof. Fail rfl. Admitted.
(** **** After importing: *)
Import Bar.
(* Availability of the tactic *)
Print find_secret.
Print Bar.find_secret.
(* Availability of the tactic notation *)
Lemma plop_i : 2 + 2 = 4.
Proof. rfl. Qed.
End InModuleDefault.
Module InModuleLocal.
Module Bar.
#[local]
Ltac2 find_secret () := rewrite secret_is_42.
#[local]
Ltac2 Notation "rfl" := reflexivity.
End Bar.
(** **** Without importing: *)
(* Availability of the tactic *)
Fail Print find_secret.
Fail Print Bar.find_secret.
(* Availability of the tactic notation *)
Lemma plop_ni : 2 + 2 = 4.
Proof. Fail rfl. Admitted.
(** **** After importing: *)
Import Bar.
(* Availability of the tactic *)
Fail Print find_secret.
Fail Print Bar.find_secret.
(* Availability of the tactic notation *)
Lemma plop_i : 2 + 2 = 4.
Proof. Fail rfl. Admitted.
End InModuleLocal.
Module InModuleExport.
Module Bar.
(* A custom tactic: *)
Fail #[export]
Ltac2 find_secret := reflexivity.
(* A tactic notation: *)
Fail #[export]
Ltac2 Notation "rfl" := reflexivity.
End Bar.
(** Nothing to check, Ltac2 and Ltac2 Notation do not support the [export]
attribute. *)
End InModuleExport.
Module InModuleGlobal.
Module Bar.
#[global]
Ltac2 find_secret () := rewrite secret_is_42.
(* A tactic notation: *)
#[global]
Ltac2 Notation "rfl" := reflexivity.
End Bar.
(** **** Without importing: *)
(* Availability of the tactic *)
Fail Print find_secret.
Print Bar.find_secret.
(* Availability of the tactic notation *)
Lemma plop_ni : 2 + 2 = 4.
Proof. Fail rfl. Admitted.
(** **** After importing: *)
Import Bar.
Print find_secret.
Print Bar.find_secret.
(* Availability of the tactic notation *)
Lemma plop_i : 2 + 2 = 4.
Proof. rfl. Qed.
End InModuleGlobal.
|
