aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/ppvernac.ml6
1 files changed, 0 insertions, 6 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 5e57f5de0..51c3eb212 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -524,12 +524,6 @@ open Decl_kinds
| VernacLocal (local, v) ->
return (pr_locality local ++ spc() ++ pr_vernac_body v)
- (* Stm *)
- | VernacStm JoinDocument ->
- return (keyword "Stm JoinDocument")
- | VernacStm Wait ->
- return (keyword "Stm Wait")
-
(* Proof management *)
| VernacAbortAll ->
return (keyword "Abort All")