aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/pp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/pp.ml')
-rw-r--r--lib/pp.ml4
1 files changed, 2 insertions, 2 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