diff options
| author | Vincent Laporte | 2018-09-06 16:07:16 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2018-09-06 16:20:43 +0200 |
| commit | af30a9a70221d8dee3b837664d372becbbf71762 (patch) | |
| tree | 331516b38190f27bbb6fe14fe06cf66f13087455 /coqpp/coqpp_parse.mly | |
| parent | 51197c3b8b5a6f30397f0263e2e2f4461519c66e (diff) | |
coqpp: allow DEPRECATED when declaring tactics
Diffstat (limited to 'coqpp/coqpp_parse.mly')
| -rw-r--r-- | coqpp/coqpp_parse.mly | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly index baafd633c4..5dc8f9374a 100644 --- a/coqpp/coqpp_parse.mly +++ b/coqpp/coqpp_parse.mly @@ -62,7 +62,7 @@ let parse_user_entry s sep = %token <string> IDENT QUALID %token <string> STRING %token <int> INT -%token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN +%token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED %token LBRACKET RBRACKET PIPE ARROW COMMA EQUAL %token LPAREN RPAREN COLON SEMICOLON %token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA @@ -108,8 +108,13 @@ vernac_extend: ; tactic_extend: -| TACTIC EXTEND IDENT tactic_level tactic_rules END - { TacticExt { tacext_name = $3; tacext_level = $4; tacext_rules = $5 } } +| TACTIC EXTEND IDENT tactic_deprecated tactic_level tactic_rules END + { TacticExt { tacext_name = $3; tacext_deprecated = $4; tacext_level = $5; tacext_rules = $6 } } +; + +tactic_deprecated: +| { None } +| DEPRECATED IDENT { Some $2 } ; tactic_level: |