diff options
| author | Pierre-Marie Pédrot | 2019-06-05 09:29:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-05 09:29:23 +0200 |
| commit | 658ae0d320473e25ee60cf158ed808be294f3a69 (patch) | |
| tree | 05c14bec8038c76f618c4f45e5a26ee89aaf7bb3 /coqpp | |
| parent | 2c6220c7973510b801d4d3c897c482b3f8c5b10d (diff) | |
| parent | 805211a603431f4ba351e0164b0bd147a771a1a0 (diff) | |
Merge PR #10307: allow empty tactic_rules in ARGUMENT EXTEND
Reviewed-by: gares
Reviewed-by: ppedrot
Diffstat (limited to 'coqpp')
| -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 } ; |