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