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 | |
| parent | 51197c3b8b5a6f30397f0263e2e2f4461519c66e (diff) | |
coqpp: allow DEPRECATED when declaring tactics
Diffstat (limited to 'coqpp')
| -rw-r--r-- | coqpp/coqpp_ast.mli | 1 | ||||
| -rw-r--r-- | coqpp/coqpp_lex.mll | 1 | ||||
| -rw-r--r-- | coqpp/coqpp_main.ml | 11 | ||||
| -rw-r--r-- | coqpp/coqpp_parse.mly | 11 |
4 files changed, 19 insertions, 5 deletions
diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli index 39b4d2ab34..8f98db705f 100644 --- a/coqpp/coqpp_ast.mli +++ b/coqpp/coqpp_ast.mli @@ -81,6 +81,7 @@ type grammar_ext = { type tactic_ext = { tacext_name : string; tacext_level : int option; + tacext_deprecated : string option; tacext_rules : tactic_rule list; } diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll index 6c6562c204..bfa4e2b57b 100644 --- a/coqpp/coqpp_lex.mll +++ b/coqpp/coqpp_lex.mll @@ -95,6 +95,7 @@ rule extend = parse | "END" { END } | "DECLARE" { DECLARE } | "PLUGIN" { PLUGIN } +| "DEPRECATED" { DEPRECATED } (** Camlp5 specific keywords *) | "GLOBAL" { GLOBAL } | "FIRST" { FIRST } diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 1648167a27..c1b94b5ebb 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -316,10 +316,17 @@ let print_rules fmt rules = fprintf fmt "Tacentries.([@[<v>%a@]])" print_rules rules let print_ast fmt ext = + let deprecation fmt = + function + | None -> () + | Some s -> fprintf fmt "~deprecation:%s " s + in let pr fmt () = let level = match ext.tacext_level with None -> 0 | Some i -> i in - fprintf fmt "Tacentries.tactic_extend %s \"%s\" ~level:%i %a" - plugin_name ext.tacext_name level print_rules ext.tacext_rules + fprintf fmt "Tacentries.tactic_extend %s \"%s\" ~level:%i %a%a" + plugin_name ext.tacext_name level + deprecation ext.tacext_deprecated + print_rules ext.tacext_rules in let () = fprintf fmt "let () = @[%a@]\n" pr () in () 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: |