Merge PR #8423: coqpp: allow DEPRECATED when declaring tactics

5 files changed, 21 insertions, 5 deletions

diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli
index 39b4d2ab34..181c43615b 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 : code 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..a8ed95f5ba 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 { code } -> fprintf fmt "~deprecation:(%s) " code
+  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..bf435fd247 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 CODE { Some $2 }
 ;
 
 tactic_level:
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index 07239e7af0..5943600b7c 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -8,6 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+(** WARNING: this file is deprecated; consider modifying coqpp instead. *)
+
 (** Implementation of the TACTIC EXTEND macro. *)
 
 open Q_util