From af30a9a70221d8dee3b837664d372becbbf71762 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 6 Sep 2018 16:07:16 +0200
Subject: coqpp: allow DEPRECATED when declaring tactics

---
 coqpp/coqpp_ast.mli   |  1 +
 coqpp/coqpp_lex.mll   |  1 +
 coqpp/coqpp_main.ml   | 11 +++++++++--
 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:
-- 
cgit v1.2.3