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.

---
 stm/texmacspp.ml         | 3 ---
 stm/vernac_classifier.ml | 1 -
 2 files changed, 4 deletions(-)

(limited to 'stm')

diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index a459cd65f8..e83313aa8e 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 97d6e1fb71..41b753fb8b 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 *)
-- 
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.

---
 stm/texmacspp.ml         | 1 -
 stm/vernac_classifier.ml | 7 -------
 2 files changed, 8 deletions(-)

(limited to 'stm')

diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index e83313aa8e..2d2ea1f8b0 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -694,7 +694,6 @@ let rec tmpp v loc =
   | VernacBackTo _ -> PCData "VernacBackTo"
 
   (* Commands *)
-  | VernacDeclareTacticDefinition _ as x -> xmlTODO loc x
   | VernacCreateHintDb _ as x -> xmlTODO loc x
   | VernacRemoveHints _ as x -> xmlTODO loc x
   | VernacHints _ as x -> xmlTODO loc x
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 41b753fb8b..ecaf0fb7c5 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -173,13 +173,6 @@ let rec classify_vernac e =
     | VernacRegister _
     | VernacNameSectionHypSet _
     | VernacComments _ -> VtSideff [], VtLater
-    | VernacDeclareTacticDefinition l ->
-        let open Libnames in
-        let open Vernacexpr in
-        VtSideff (List.map (function
-          | TacticDefinition ((_,r),_) -> r
-          | TacticRedefinition (Ident (_,r),_) -> r
-          | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater
     (* Who knows *)
     | VernacLoad _ -> VtSideff [], VtNow
     (* (Local) Notations have to disappear *)
-- 
cgit v1.2.3