blob: d22b7ed16c13c5015d1c017ba27943aaeb36cd3e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
Grammar vernac vernac : ast :=
add_dad_rule00 ["AddDadRule" stringarg($name) constrarg($pat)
"first_path" "second_path" tacarg($tac) "."] ->
[(AddDadRule $name $pat (NUMBERLIST) (NUMBERLIST) (TACTIC $tac))].
Grammar vernac vernac:ast :=
| add_dad_rule01 ["AddDadRule" stringarg($name) constrarg($pat)
"first_path" "second_path" ne_numarg_list($l) tacarg($tac) "."] ->
[(AddDadRule $name $pat (NUMBERLIST) (NUMBERLIST ($LIST $l)) (TACTIC $tac))]
| add_dad_rule10 ["AddDadRule" stringarg($name) constrarg($pat)
"first_path" ne_numarg_list($l) "second_path" tacarg($tac) "."] ->
[(AddDadRule $name $pat (NUMBERLIST ($LIST $l))(NUMBERLIST) (TACTIC $tac))]
| add_dad_rule11 ["AddDadRule" stringarg($name) constrarg($pat)
"first_path" ne_numarg_list($l) "second_path" ne_numarg_list($l1)
tacarg($tac) "."] ->
[(AddDadRule $name $pat (NUMBERLIST ($LIST $l))(NUMBERLIST ($LIST $l1))
(TACTIC $tac))].
Grammar vernac vernac : ast :=
start_dad [ "StartDad" "."] -> [(StartDad)].
|
