[pp] Make pp public to allow serialization.

2 files changed, 24 insertions, 7 deletions

diff --git a/lib/pp.ml b/lib/pp.ml
index 6d7bdf75e..140ad4e22 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -19,14 +19,14 @@ open Pp_control
    \end{description}
  *)
 
+type pp_tag = string list
+
 type block_type =
   | Pp_hbox   of int
   | Pp_vbox   of int
   | Pp_hvbox  of int
   | Pp_hovbox of int
 
-type pp_tag = string list
-
 type std_ppcmds =
   | Ppcmd_empty
   | Ppcmd_string of string
diff --git a/lib/pp.mli b/lib/pp.mli
index f61261a17..2b2017926 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -6,9 +6,29 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Pretty-printers. *)
+(** Coq document type. *)
 
-type std_ppcmds
+(* XXX: Improve and add attributes *)
+type pp_tag = string list
+
+type block_type =
+  | Pp_hbox   of int
+  | Pp_vbox   of int
+  | Pp_hvbox  of int
+  | Pp_hovbox of int
+
+type std_ppcmds =
+  | Ppcmd_empty
+  | Ppcmd_string of string
+  | Ppcmd_glue of std_ppcmds * std_ppcmds
+  | Ppcmd_box  of block_type * std_ppcmds
+  | Ppcmd_print_break of int * int
+  | Ppcmd_white_space of int
+  | Ppcmd_force_newline
+  | Ppcmd_open_box of block_type
+  | Ppcmd_close_box
+  | Ppcmd_open_tag of pp_tag
+  | Ppcmd_close_tag
 
 (** {6 Formatting commands} *)
 
@@ -59,9 +79,6 @@ val close : unit -> std_ppcmds
 
 (** {6 Opening and closing of tags} *)
 
-(* XXX: Improve and add attributes *)
-type pp_tag = string list
-
 val tag : pp_tag -> std_ppcmds -> std_ppcmds
 val open_tag : pp_tag -> std_ppcmds
 val close_tag : unit -> std_ppcmds