From 3b3d5937939ac8dc4f152d61391630e62bb0b2e5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 7 Dec 2016 12:12:54 +0100 Subject: [pp] [ide] Minor cleanups in pp code. - We avoid unnecessary use of Pp -> string conversion functions. and the creation of intermediate buffers on logging. - We rename local functions that share the name with the Coq stdlib, this is usually dangerous as if the normal function is removed, code may pick up the one in the stdlib, with different semantics. --- ide/minilib.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'ide/minilib.mli') diff --git a/ide/minilib.mli b/ide/minilib.mli index b7672c900..4517a2374 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -22,7 +22,8 @@ type level = [ (** debug printing *) val debug : bool ref -val log : ?level:level -> string -> unit +val log_pp : ?level:level -> Pp.std_ppcmds -> unit +val log : ?level:level -> string -> unit val coqide_config_home : unit -> string val coqide_config_dirs : unit -> string list -- cgit v1.2.3