diff options
Diffstat (limited to 'ide/minilib.mli')
| -rw-r--r-- | ide/minilib.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/minilib.mli b/ide/minilib.mli index 4517a2374..c96e59b22 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -22,7 +22,7 @@ type level = [ (** debug printing *) val debug : bool ref -val log_pp : ?level:level -> Pp.std_ppcmds -> unit +val log_pp : ?level:level -> Pp.t -> unit val log : ?level:level -> string -> unit val coqide_config_home : unit -> string |