diff options
| author | Pierre-Marie Pédrot | 2016-03-20 02:23:21 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-20 02:41:58 +0100 |
| commit | 4f52bd681ad9bbcbbd68406a58b47d8e962336ed (patch) | |
| tree | 5b891de8b42d9cb20ec3273ae1e02bd586f42fd0 /stm | |
| parent | 9f5d9cd2622f3890e70dad01898868fe29df6048 (diff) | |
Moving the Ltac definition command to an EXTEND based command.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/texmacspp.ml | 1 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 7 |
2 files changed, 0 insertions, 8 deletions
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 *) |