aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/texmacspp.ml3
1 files changed, 0 insertions, 3 deletions
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index 680da7f54b..dbcd8630b1 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