diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/texmacspp.ml | 4 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 8 |
2 files changed, 0 insertions, 12 deletions
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index a459cd65f8..2d2ea1f8b0 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 @@ -697,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 97d6e1fb71..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 *) @@ -195,7 +188,6 @@ let rec classify_vernac e = | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ | VernacSyntaxExtension _ | VernacSyntacticDefinition _ - | VernacTacticNotation _ | VernacRequire _ | VernacImport _ | VernacInclude _ | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) |