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