diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-30 00:00:44 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-30 00:00:44 +0200 |
| commit | 298b0a90e0393f3af16fd0b5870128212518a1a4 (patch) | |
| tree | 9d359ac8e567d8634e5a596b49c296414bcf606a /printing | |
| parent | df78cb79c549c7dc02e2f19add28be3600d3565f (diff) | |
| parent | 584a832d4f681d34c7cbdd87d9ceb7a742b39959 (diff) | |
Merge PR#511: [stm] Remove some obsolete vernacs/classification.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 78ef4d4ba..cfc2e48d1 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -534,18 +534,8 @@ open Decl_kinds (* Stm *) | VernacStm JoinDocument -> return (keyword "Stm JoinDocument") - | VernacStm PrintDag -> - return (keyword "Stm PrintDag") - | VernacStm Finish -> - return (keyword "Stm Finish") | VernacStm Wait -> return (keyword "Stm Wait") - | VernacStm (Observe id) -> - return (keyword "Stm Observe " ++ str(Stateid.to_string id)) - | VernacStm (Command v) -> - return (keyword "Stm Command " ++ pr_vernac_body v) - | VernacStm (PGLast v) -> - return (keyword "Stm PGLast " ++ pr_vernac_body v) (* Proof management *) | VernacAbortAll -> |