diff options
Diffstat (limited to 'lib/pp.ml')
-rw-r--r-- | lib/pp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -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 |