From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 grammar/tacextend.mlp | 31 +++++++++----------------------
 1 file changed, 9 insertions(+), 22 deletions(-)

(limited to 'grammar/tacextend.mlp')

diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index 525be643..5943600b 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
@@ -15,32 +17,13 @@ open Argextend
 
 let plugin_name = <:expr< __coq_plugin_name >>
 
-let mlexpr_of_ident id =
-  (** Workaround for badly-designed generic arguments lacking a closure *)
-  let id = "$" ^ id in
-  <:expr< Names.Id.of_string_soft $str:id$ >>
-
-let rec mlexpr_of_symbol = function
-| Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >>
-| Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >>
-| Ulist0 s -> <:expr< Extend.TUlist0 $mlexpr_of_symbol s$ >>
-| Ulist0sep (s,sep) -> <:expr< Extend.TUlist0sep $mlexpr_of_symbol s$ $str:sep$ >>
-| Uopt s -> <:expr< Extend.TUopt $mlexpr_of_symbol s$ >>
-| Uentry e ->
-  let wit = <:expr< $lid:"wit_"^e$ >> in
-  <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >>
-| Uentryl (e, l) ->
-  assert (e = "tactic");
-  let wit = <:expr< $lid:"wit_"^e$ >> in
-  <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>>
-
 let rec mlexpr_of_clause = function
 | [] -> <:expr< TyNil >>
 | ExtTerminal s :: cl -> <:expr< TyIdent($str:s$, $mlexpr_of_clause cl$) >>
 | ExtNonTerminal(g,None) :: cl ->
-  <:expr< TyAnonArg(Loc.tag($mlexpr_of_symbol g$), $mlexpr_of_clause cl$) >>
+  <:expr< TyAnonArg($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >>
 | ExtNonTerminal(g,Some id) :: cl ->
-  <:expr< TyArg(Loc.tag($mlexpr_of_symbol g$, $mlexpr_of_ident id$), $mlexpr_of_clause cl$) >>
+  <:expr< TyArg($mlexpr_of_symbol g$, $mlexpr_of_string id$, $mlexpr_of_clause cl$) >>
 
 let rec binders_of_clause e = function
 | [] -> <:expr< fun ist -> $e$ >>
@@ -54,13 +37,17 @@ EXTEND
   GLOBAL: str_item;
   str_item:
     [ [ "TACTIC"; "EXTEND"; s = tac_name;
+        depr = OPT [ "DEPRECATED"; depr = LIDENT -> depr ];
         level = OPT [ "AT"; UIDENT "LEVEL"; level = INT -> level ];
         OPT "|"; l = LIST1 tacrule SEP "|";
         "END" ->
         let level = match level with Some i -> int_of_string i | None -> 0 in
         let level = mlexpr_of_int level in
+        let depr = mlexpr_of_option (fun l -> <:expr< $lid:l$ >>) depr in
         let l = <:expr< Tacentries.($mlexpr_of_list (fun x -> x) l$) >> in
-        declare_str_items loc [ <:str_item< Tacentries.tactic_extend $plugin_name$ $str:s$ ~{ level = $level$ } $l$ >> ] ] ]
+        declare_str_items loc [ <:str_item< Tacentries.tactic_extend
+          $plugin_name$ $str:s$ ~{ level = $level$ } ?{ deprecation =
+          $depr$ } $l$ >> ] ] ]
   ;
   tacrule:
     [ [ "["; l = LIST1 tacargs; "]";
-- 
cgit v1.2.3