blob: 20301ec4f5644f57a4f68b384da56050ef62bb7d (
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
|
(* Printing all kinds of Ltac generic arguments *)
Tactic Notation "myidtac" string(v) := idtac v.
Goal True.
myidtac "foo".
Abort.
Tactic Notation "myidtac2" ref(c) := idtac c.
Goal True.
myidtac2 True.
Abort.
Tactic Notation "myidtac3" preident(s) := idtac s.
Goal True.
myidtac3 foo.
Abort.
Tactic Notation "myidtac4" int_or_var(n) := idtac n.
Goal True.
myidtac4 3.
Abort.
Tactic Notation "myidtac5" ident(id) := idtac id.
Goal True.
myidtac5 foo.
Abort.
|
