diff options
| author | Dabrowski | 2019-06-05 00:00:18 +0200 |
|---|---|---|
| committer | Dabrowski | 2019-06-05 00:00:18 +0200 |
| commit | 805211a603431f4ba351e0164b0bd147a771a1a0 (patch) | |
| tree | 51cd3a8bc35af767d8bdd1dee80e48539459cb46 /coqpp/coqpp_parse.mly | |
| parent | e9c42c26d1fc653d1411fa2fe41b12bffa8ae992 (diff) | |
allow empty tactic_rules in ARGUMENT EXTEND
Diffstat (limited to 'coqpp/coqpp_parse.mly')
| -rw-r--r-- | coqpp/coqpp_parse.mly | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly index 43ba990f6a..f7959f8201 100644 --- a/coqpp/coqpp_parse.mly +++ b/coqpp/coqpp_parse.mly @@ -270,7 +270,7 @@ tactic_level: ; tactic_rules: -| tactic_rule { [$1] } +| { [] } | tactic_rule tactic_rules { $1 :: $2 } ; |