Getting rid of Pp.msg

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15400 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 13 insertions, 7 deletions

diff --git a/lib/pp.mli b/lib/pp.mli
index da37a1153..135343092 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