aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-18 13:27:20 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-19 11:43:42 +0200
commit84accdaea3ce094cc5d0232107d3e2ea654a76c2 (patch)
treeeab140c332984b597536d1cabdf9b2ecd474b929 /printing
parentd87bc5b9fb353655f8b905d73293abe96b0ad063 (diff)
Remove STM vernaculars.
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")