From 0af598b77a6242d796c66884477a046448ef1e21 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 01:31:43 +0100
Subject: Moving Tactic Notation to an EXTEND based command.

---
 printing/ppvernac.ml | 13 -------------
 1 file changed, 13 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 887a14d2bf..88bb805a72 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 ") ++
-- 
cgit v1.2.3


From 01cd0dd64e4faa52b5094a99e2c31ecc4e7b767d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 02:09:54 +0100
Subject: Moving Print Ltac to an EXTEND based command.

---
 printing/ppvernac.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 88bb805a72..edd32e8337 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -455,8 +455,6 @@ module Make
         keyword "Print TypeClasses"
       | PrintInstances qid ->
         keyword "Print Instances" ++ spc () ++ pr_smart_global qid
-      | PrintLtac qid ->
-        keyword "Print Ltac" ++ spc() ++ pr_ltac_ref qid
       | PrintCoercions ->
         keyword "Print Coercions"
       | PrintCoercionPaths (s,t) ->
-- 
cgit v1.2.3


From 4f52bd681ad9bbcbbd68406a58b47d8e962336ed Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 02:23:21 +0100
Subject: Moving the Ltac definition command to an EXTEND based command.

---
 printing/ppvernac.ml | 23 -----------------------
 1 file changed, 23 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index edd32e8337..c1f5e122bd 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -995,29 +995,6 @@ module Make
           return (keyword "Cd" ++ pr_opt qs s)
 
         (* Commands *)
-        | VernacDeclareTacticDefinition l ->
-          let pr_tac_body tacdef_body =
-            let id, redef, body =
-              match tacdef_body with
-              | TacticDefinition ((_,id), body) -> pr_id id, false, body
-              | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body
-            in
-            let idl, body =
-              match body with
-                | Tacexpr.TacFun (idl,b) -> idl,b
-                | _ -> [], body in
-            id ++
-              prlist (function None -> str " _"
-                | Some id -> spc () ++ pr_id id) idl
-            ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++
-              pr_raw_tactic body
-          in
-          return (
-            hov 1
-              (keyword "Ltac" ++ spc () ++
-                 prlist_with_sep (fun () ->
-                   fnl() ++ keyword "with" ++ spc ()) pr_tac_body l)
-          )
         | VernacCreateHintDb (dbname,b) ->
           return (
             hov 1 (keyword "Create HintDb" ++ spc () ++
-- 
cgit v1.2.3