diff options
Diffstat (limited to 'coqpp/coqpp_parse.mly')
| -rw-r--r-- | coqpp/coqpp_parse.mly | 29 |
1 files changed, 23 insertions, 6 deletions
diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly index 1fb5461b21..abe52ab46b 100644 --- a/coqpp/coqpp_parse.mly +++ b/coqpp/coqpp_parse.mly @@ -65,7 +65,7 @@ let parse_user_entry s sep = %token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED ARGUMENT %token RAW_PRINTED GLOB_PRINTED %token COMMAND CLASSIFIED PRINTED TYPED INTERPRETED GLOBALIZED SUBSTITUTED BY AS -%token LBRACKET RBRACKET PIPE ARROW FUN COMMA EQUAL STAR +%token HASHBRACKET LBRACKET RBRACKET PIPE ARROW FUN COMMA EQUAL STAR %token LPAREN RPAREN COLON SEMICOLON %token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA %token EOF @@ -209,15 +209,32 @@ vernac_rules: ; vernac_rule: -| PIPE LBRACKET ext_tokens RBRACKET rule_deprecation rule_classifier ARROW CODE +| PIPE vernac_attributes_opt LBRACKET ext_tokens RBRACKET rule_deprecation rule_classifier ARROW CODE { { - vernac_toks = $3; - vernac_depr = $5; - vernac_class= $6; - vernac_body = $8; + vernac_atts = $2; + vernac_toks = $4; + vernac_depr = $6; + vernac_class= $7; + vernac_body = $9; } } ; +vernac_attributes_opt: +| { None } +| HASHBRACKET vernac_attributes RBRACKET { Some $2 } +; + +vernac_attributes: +| vernac_attribute { [$1] } +| vernac_attribute SEMICOLON { [$1] } +| vernac_attribute SEMICOLON vernac_attributes { $1 :: $3 } +; + +vernac_attribute: +| qualid_or_ident EQUAL qualid_or_ident { ($1, $3) } +| qualid_or_ident { ($1, $1) } +; + rule_deprecation: | { false } | DEPRECATED { true } |