aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/texmacspp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/texmacspp.ml')
-rw-r--r--ide/texmacspp.ml3
1 files changed, 0 insertions, 3 deletions
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index 680da7f54..dbcd8630b 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -724,9 +724,6 @@ let rec tmpp v loc =
| VernacComments (cl) ->
xmlComment loc (List.flatten (List.map pp_comment cl))
- (* Stm backdoor *)
- | VernacStm _ as x -> xmlTODO loc x
-
(* Proof management *)
| VernacGoal _ as x -> xmlTODO loc x
| VernacAbort _ as x -> xmlTODO loc x