From 4d58a4f25a796d1c5d39f2be8648696cdfd46dba Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Wed, 30 May 2012 16:51:34 +0000
Subject: Getting rid of Pp.msg

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15400 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/pp.mli | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

(limited to 'lib/pp.mli')

diff --git a/lib/pp.mli b/lib/pp.mli
index da37a11533..135343092d 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -96,6 +96,9 @@ val msgnl_with : Format.formatter -> std_ppcmds -> unit
 
 (** {6 Pretty-printing functions {% \emph{%}without flush{% }%} on [stdout] and [stderr]. } *)
 
+(** These functions are low-level interace to printing and should not be used
+    in usual code. Consider using the [msg_*] function family instead. *)
+
 val pp : std_ppcmds -> unit
 val ppnl : std_ppcmds -> unit
 val pperr : std_ppcmds -> unit
@@ -104,19 +107,22 @@ val message : string -> unit       (** = pPNL *)
 val pp_flush : unit -> unit
 val flush_all: unit -> unit
 
-(** {6 Pretty-printing functions {% \emph{%}with flush{% }%} on [stdout] and [stderr]. } *)
+(** {6 Sending messages to the user } *)
 
-val msg : std_ppcmds -> unit
-val msgnl : std_ppcmds -> unit
-val msgerr : std_ppcmds -> unit
-val msgerrnl : std_ppcmds -> unit
+val msg_info : std_ppcmds -> unit
 val msg_warning : std_ppcmds -> unit
-
-(** Same specific display in emacs as warning, but without the "Warning:" **)
 val msg_debug : std_ppcmds -> unit
 
 val string_of_ppcmds : std_ppcmds -> string
 
+(** {6 Deprecated functions} *)
+
+(** DEPRECATED. Do not use in newly written code. *)
+val msg : std_ppcmds -> unit
+val msgnl : std_ppcmds -> unit
+val msgerr : std_ppcmds -> unit
+val msgerrnl : std_ppcmds -> unit
+
 (** {6 Location management. } *)
 
 type loc = Loc.t
-- 
cgit v1.2.3