Moving Tactic Notation to an EXTEND based command.

7 files changed, 35 insertions, 36 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 36b855ec3..123b3ec1b 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -291,8 +291,6 @@ type vernac_expr =
   | VernacError of exn (* always fails *)
 
   (* Syntax *)
-  | VernacTacticNotation of
-      int * grammar_tactic_prod_item_expr list * raw_tactic_expr
   | VernacSyntaxExtension of
       obsolete_locality * (lstring * syntax_modifier list)
   | VernacOpenCloseScope of obsolete_locality * (bool * scope_name)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c89238d29..3b5d276dd 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1048,10 +1048,6 @@ GEXTEND Gram
      | IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING ->
            VernacNotationAddFormat (n,s,fmt)
 
-     | IDENT "Tactic"; IDENT "Notation"; n = tactic_level;
-	 pil = LIST1 production_item; ":="; t = Tactic.tactic
-         -> VernacTacticNotation (n,pil,t)
-
      | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring;
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] ->
 	   Metasyntax.check_infix_modifiers l;
@@ -1077,9 +1073,6 @@ GEXTEND Gram
   obsolete_locality:
     [ [ IDENT "Local" -> true | -> false ] ]
   ;
-  tactic_level:
-    [ [ "("; "at"; IDENT "level"; n = natural; ")" -> n | -> 0 ] ]
-  ;
   level:
     [ [ IDENT "level"; n = natural -> NumLevel n
       | IDENT "next"; IDENT "level" -> NextLevel ] ]
@@ -1111,10 +1104,4 @@ GEXTEND Gram
       | IDENT "closed"; IDENT "binder" -> ETBinder false
     ] ]
   ;
-  production_item:
-    [ [ s = ne_string -> TacTerm s
-      | nt = IDENT;
-        po = [ "("; p = ident; sep = [ -> "" | ","; sep = STRING -> sep ];
-                   ")" -> (p,sep) ] -> TacNonTerm (!@loc,nt,po) ] ]
-  ;
 END
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 887a14d2b..88bb805a7 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -378,17 +378,6 @@ module Make
     | l -> spc() ++
       hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
 
-  let print_level n =
-    if not (Int.equal n 0) then
-      spc () ++ tag_keyword (str "(at level " ++ int n ++ str ")")
-    else
-      mt ()
-
-  let pr_grammar_tactic_rule n (_,pil,t) =
-    hov 2 (keyword "Tactic Notation" ++ print_level n ++ spc() ++
-             hov 0 (prlist_with_sep sep pr_production_item pil ++
-                      spc() ++ str":=" ++ spc() ++ pr_raw_tactic t))
-
   let pr_univs pl =
     match pl with
     | None -> mt ()
@@ -644,8 +633,6 @@ module Make
           return (keyword "No-parsing-rule for VernacError")
 
       (* Syntax *)
-        | VernacTacticNotation (n,r,e) ->
-          return (pr_grammar_tactic_rule n ("",r,e))
         | VernacOpenCloseScope (_,(opening,sc)) ->
           return (
             keyword (if opening then "Open " else "Close ") ++
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index a459cd65f..e83313aa8 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -503,9 +503,6 @@ let rec tmpp v loc =
   | VernacError _ -> xmlWithLoc loc "error" [] []
 
   (* Syntax *)
-  | VernacTacticNotation _ as x ->
-      xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
   | VernacSyntaxExtension (_, ((_, name), sml)) ->
       let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
       xmlReservedNotation attrs name loc
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 97d6e1fb7..41b753fb8 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -195,7 +195,6 @@ let rec classify_vernac e =
     | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
     | VernacSyntaxExtension _ 
     | VernacSyntacticDefinition _
-    | VernacTacticNotation _
     | VernacRequire _ | VernacImport _ | VernacInclude _
     | VernacDeclareMLModule _
     | VernacContext _ (* TASSI: unsure *)
diff --git a/tactics/g_ltac.ml4 b/tactics/g_ltac.ml4
index d1992c57b..3573ca717 100644
--- a/tactics/g_ltac.ml4
+++ b/tactics/g_ltac.ml4
@@ -370,3 +370,37 @@ VERNAC tactic_mode EXTEND VernacSolve
     vernac_solve SelectAll n t def
   ]
 END
+
+let pr_ltac_tactic_level n = str "(at level " ++ int n ++ str ")"
+
+VERNAC ARGUMENT EXTEND ltac_tactic_level PRINTED BY pr_ltac_tactic_level
+| [ "(" "at" "level" natural(n) ")" ] -> [ n ]
+END
+
+VERNAC ARGUMENT EXTEND ltac_production_sep
+| [ "," string(sep) ] -> [ sep ]
+END
+
+let pr_ltac_production_item = function
+| TacTerm s -> quote (str s)
+| TacNonTerm (_, arg, (id, sep)) ->
+  let sep = match sep with
+  | "" -> mt ()
+  | sep -> str "," ++ spc () ++ quote (str sep)
+  in
+  str arg ++ str "(" ++ Nameops.pr_id id ++ sep ++ str ")"
+
+VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item
+| [ string(s) ] -> [ TacTerm s ]
+| [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] ->
+  [ TacNonTerm (loc, Names.Id.to_string nt, (p, Option.default "" sep)) ]
+END
+
+VERNAC COMMAND EXTEND VernacTacticNotation CLASSIFIED AS SIDEFF
+| [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] ->
+  [
+    let l = Locality.LocalityFixme.consume () in
+    let n = Option.default 0 n in
+    Metasyntax.add_tactic_notation (Locality.make_module_locality l, n, r, e)
+  ]
+END
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 64f9cd9ca..bdf0ada2c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1822,8 +1822,6 @@ let interp ?proof ~loc locality poly c =
   | VernacError e -> raise e
 
   (* Syntax *)
-  | VernacTacticNotation (n,r,e) ->
-      Metasyntax.add_tactic_notation (make_module_locality locality,n,r,e)
   | VernacSyntaxExtension (local,sl) ->
       vernac_syntax_extension locality local sl
   | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
@@ -1978,8 +1976,7 @@ let check_vernac_supports_locality c l =
   match l, c with
   | None, _ -> ()
   | Some _, (
-      VernacTacticNotation _
-    | VernacOpenCloseScope _
+      VernacOpenCloseScope _
     | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _
     | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _
     | VernacAssumption _ | VernacStartTheoremProof _