blob: 2810f4cc52b501f6b89c6baf203dee3df5cfa70d (
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
|
Declare ML Module "autorewrite".
Grammar vernac orient : ast :=
| lr ["->"] -> ["LR"]
| rl ["<-"] -> ["RL"]
| ng [] -> ["LR"]
with vernac : ast :=
| hint_rew_b [ "Hint" "Rewrite" orient($o) "[" ne_constrarg_list($l) "]" "in"
identarg($b) "."] ->
[ (HintRewrite $o (CONSTRLIST ($LIST $l)) $b (TACTIC (Idtac))) ]
| hint_rew_t [ "Hint" "Rewrite" orient($o) "[" ne_constrarg_list($l) "]" "in"
identarg($b) "using" tacarg($t) "." ] ->
[ (HintRewrite $o (CONSTRLIST ($LIST $l)) $b (TACTIC $t)) ].
Grammar tactic simple_tactic : ast :=
| auto_rew_b [ "AutoRewrite" "[" ne_identarg_list($l) "]" ] ->
[ (AutoRewrite ($LIST $l)) ]
| auto_rew_t [ "AutoRewrite" "[" ne_identarg_list($l) "]" "using"
tactic($t) ] -> [ (AutoRewrite (TACTIC $t) ($LIST $l)) ].
Syntax tactic level 0:
| auto_rew_b [<<(AutoRewrite $l)>>] ->
[ "AutoRewrite" [1 0] "[" [1 0] $l [1 0] "]" ]
| auto_rew_t [<<(AutoRewrite $t $l)>>] ->
[ "AutoRewrite" [1 0] "[" [1 0] $l [1 0] "]" [1 0] "using" [1 0] $t ].
|
