aboutsummaryrefslogtreecommitdiff
path: root/ide/ideutils.mli
diff options
context:
space:
mode:
Diffstat (limited to 'ide/ideutils.mli')
-rw-r--r--ide/ideutils.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 4b4ba72b0b..f06a48aebe 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -67,7 +67,7 @@ val requote : string -> string
val textview_width : #GText.view_skel -> int
(** Returns an approximate value of the character width of a textview *)
-type logger = Feedback.level -> Pp.std_ppcmds -> unit
+type logger = Feedback.level -> Pp.t -> unit
val default_logger : logger
(** Default logger. It logs messages that the casual user should not see. *)