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


From 1877e1235c63ff3bbc958e5a79fa052ac852071c Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 6 Sep 2018 17:26:47 +0200
Subject: deprecation is CODE instead of IDENT

---
 coqpp/coqpp_ast.mli   | 2 +-
 coqpp/coqpp_main.ml   | 2 +-
 coqpp/coqpp_parse.mly | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli
index 8f98db705f..181c43615b 100644
--- a/coqpp/coqpp_ast.mli
+++ b/coqpp/coqpp_ast.mli
@@ -81,7 +81,7 @@ type grammar_ext = {
 type tactic_ext = {
   tacext_name : string;
   tacext_level : int option;
-  tacext_deprecated : string option;
+  tacext_deprecated : code option;
   tacext_rules : tactic_rule list;
 }
 
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index c1b94b5ebb..a8ed95f5ba 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -319,7 +319,7 @@ let print_ast fmt ext =
   let deprecation fmt =
     function
     | None -> ()
-    | Some s -> fprintf fmt "~deprecation:%s " s
+    | Some { code } -> fprintf fmt "~deprecation:(%s) " code
   in
   let pr fmt () =
     let level = match ext.tacext_level with None -> 0 | Some i -> i in
diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly
index 5dc8f9374a..bf435fd247 100644
--- a/coqpp/coqpp_parse.mly
+++ b/coqpp/coqpp_parse.mly
@@ -114,7 +114,7 @@ tactic_extend:
 
 tactic_deprecated:
 | { None }
-| DEPRECATED IDENT { Some $2 }
+| DEPRECATED CODE { Some $2 }
 ;
 
 tactic_level:
-- 
cgit v1.2.3


From f6ed48098636f11362945d380bbe8cb71a9ab2ee Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 6 Sep 2018 17:28:38 +0200
Subject: Deprecation warning in legacy tacextend.mlp

---
 grammar/tacextend.mlp | 2 ++
 1 file changed, 2 insertions(+)

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
-- 
cgit v1.2.3