summaryrefslogtreecommitdiff
path: root/src/print.sig
diff options
context:
space:
mode:
Diffstat (limited to 'src/print.sig')
-rw-r--r--src/print.sig10
1 files changed, 7 insertions, 3 deletions
diff --git a/src/print.sig b/src/print.sig
index 5bf3fcd8..39daf5d0 100644
--- a/src/print.sig
+++ b/src/print.sig
@@ -48,7 +48,11 @@ signature PRINT = sig
val preface : string * PD.pp_desc -> unit
val epreface : string * PD.pp_desc -> unit
- val fprefaces : PD.PPS.stream -> (string * PD.pp_desc) list -> unit
- val prefaces : (string * PD.pp_desc) list -> unit
- val eprefaces : (string * PD.pp_desc) list -> unit
+ val fprefaces : PD.PPS.stream -> string -> (string * PD.pp_desc) list -> unit
+ val prefaces : string -> (string * PD.pp_desc) list -> unit
+ val eprefaces : string -> (string * PD.pp_desc) list -> unit
+
+ val fprefaces' : PD.PPS.stream -> (string * PD.pp_desc) list -> unit
+ val prefaces' : (string * PD.pp_desc) list -> unit
+ val eprefaces' : (string * PD.pp_desc) list -> unit
end