From 6c521565323ae8af22fb03e65664ef944da6ecdf Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Fri, 30 Sep 2016 17:12:11 +0200
Subject: [pp] Force well-tagged docs by construction.

We replace open/close tag commands by a well-balanced "tag" wrapper.
---
 lib/pp.mli | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'lib/pp.mli')

diff --git a/lib/pp.mli b/lib/pp.mli
index bd8509dbc..ed97226ae 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -27,8 +27,8 @@ type std_ppcmds =
   | Ppcmd_force_newline
   | Ppcmd_open_box of block_type
   | Ppcmd_close_box
-  | Ppcmd_open_tag of pp_tag
-  | Ppcmd_close_tag
+  | Ppcmd_comment of string list
+  | Ppcmd_tag of pp_tag * std_ppcmds
 
 (** {6 Formatting commands} *)
 
@@ -80,8 +80,6 @@ val close : unit -> std_ppcmds
 (** {6 Opening and closing of tags} *)
 
 val tag : pp_tag -> std_ppcmds -> std_ppcmds
-val open_tag : pp_tag -> std_ppcmds
-val close_tag : unit -> std_ppcmds
 
 (** {6 Printing combinators} *)
 
-- 
cgit v1.2.3