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

---
 plugins/ltac/extraargs.ml4 | 51 +++++++---------------------------------------
 1 file changed, 7 insertions(+), 44 deletions(-)

(limited to 'plugins/ltac/extraargs.ml4')

diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 702b8303..d7799511 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -19,7 +19,6 @@ open Tacmach
 open Tacexpr
 open Taccoerce
 open Tacinterp
-open Misctypes
 open Locus
 
 (** Adding scopes for generic arguments not defined through ARGUMENT EXTEND *)
@@ -35,7 +34,7 @@ let () = create_generic_quotation "ident" Pcoq.Prim.ident Stdarg.wit_ident
 let () = create_generic_quotation "reference" Pcoq.Prim.reference Stdarg.wit_ref
 let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Stdarg.wit_uconstr
 let () = create_generic_quotation "constr" Pcoq.Constr.lconstr Stdarg.wit_constr
-let () = create_generic_quotation "ipattern" Pltac.simple_intropattern Stdarg.wit_intro_pattern
+let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_intro_pattern
 let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Stdarg.wit_open_constr
 let () =
   let inject (loc, v) = Tacexpr.Tacexp v in
@@ -53,8 +52,11 @@ let () =
 
 (* Rewriting orientation *)
 
-let _ = Metasyntax.add_token_obj "<-"
-let _ = Metasyntax.add_token_obj "->"
+let _ =
+  Mltop.declare_cache_obj
+    (fun () -> Metasyntax.add_token_obj "<-";
+               Metasyntax.add_token_obj "->")
+    "ltac_plugin"
 
 let pr_orient _prc _prlc _prt = function
   | true -> Pp.mt ()
@@ -251,7 +253,7 @@ END
 let pr_by_arg_tac _prc _prlc prtac opt_c =
   match opt_c with
     | None -> mt ()
-    | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_term.E) t)
+    | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_gram.E) t)
 
 ARGUMENT EXTEND by_arg_tac
   TYPED AS tactic_opt
@@ -298,25 +300,6 @@ END
 
 (* spiwack: the print functions are incomplete, but I don't know what they are
 	used for *)
-let pr_r_nat_field natf =
-  str "nat " ++
-  match natf with
-    | Retroknowledge.NatType -> str "type"
-    | Retroknowledge.NatPlus -> str "plus"
-    | Retroknowledge.NatTimes -> str "times"
-
-let pr_r_n_field  nf =
-  str "binary N " ++
-  match nf with
-    | Retroknowledge.NPositive -> str "positive"
-    | Retroknowledge.NType -> str "type"
-    | Retroknowledge.NTwice -> str "twice"
-    | Retroknowledge.NTwicePlusOne -> str "twice plus one"
-    | Retroknowledge.NPhi -> str "phi"
-    | Retroknowledge.NPhiInv -> str "phi inv"
-    | Retroknowledge.NPlus -> str "plus"
-    | Retroknowledge.NTimes -> str "times"
-
 let pr_r_int31_field i31f =
   str "int31 " ++
   match i31f with
@@ -354,26 +337,6 @@ let pr_retroknowledge_field f =
   | Retroknowledge.KInt31 (group, i31f) -> (pr_r_int31_field i31f) ++
                                            spc () ++ str "in " ++ qs group
 
-VERNAC ARGUMENT EXTEND retroknowledge_nat
-PRINTED BY pr_r_nat_field
-| [ "nat" "type" ] -> [ Retroknowledge.NatType ]
-| [ "nat" "plus" ] -> [ Retroknowledge.NatPlus ]
-| [ "nat" "times" ] -> [ Retroknowledge.NatTimes ]
-END
-
-
-VERNAC ARGUMENT EXTEND retroknowledge_binary_n
-PRINTED BY pr_r_n_field
-| [ "binary" "N" "positive" ] -> [ Retroknowledge.NPositive ]
-| [ "binary" "N" "type" ] -> [ Retroknowledge.NType ]
-| [ "binary" "N" "twice" ] -> [ Retroknowledge.NTwice ]
-| [ "binary" "N" "twice" "plus" "one" ] -> [ Retroknowledge.NTwicePlusOne ]
-| [ "binary" "N" "phi" ] -> [ Retroknowledge.NPhi ]
-| [ "binary" "N" "phi" "inv" ] -> [ Retroknowledge.NPhiInv ]
-| [ "binary" "N" "plus" ] -> [ Retroknowledge.NPlus ]
-| [ "binary" "N" "times" ] -> [ Retroknowledge.NTimes ]
-END
-
 VERNAC ARGUMENT EXTEND retroknowledge_int31
 PRINTED BY pr_r_int31_field
 | [ "int31" "bits" ] -> [ Retroknowledge.Int31Bits ]
-- 
cgit v1.2.3