Getting rid of Pp.msgnl and Pp.message.

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

3 files changed, 8 insertions, 8 deletions

diff --git a/lib/compat.ml4 b/lib/compat.ml4
index 8d8483b49f..9f54512a1f 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -109,7 +109,7 @@ module type GrammarSig = sig
   val action : 'a -> action
   val entry_create : string -> 'a entry
   val entry_parse : 'a entry -> parsable -> 'a
-  val entry_print : 'a entry -> unit
+  val entry_print : Format.formatter -> 'a entry -> unit
   val srules' : production_rule list -> symbol
   val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
 end
@@ -129,9 +129,9 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
   let entry_create = Entry.create
   let entry_parse = Entry.parse
 IFDEF CAMLP5_6_02_1 THEN
-  let entry_print x = Entry.print !Pp_control.std_ft x
+  let entry_print ft x = Entry.print ft x
 ELSE
-  let entry_print = Entry.print
+  let entry_print _ x = Entry.print x
 END
   let srules' = Gramext.srules
   let parse_tokens_after_filter = Entry.parse_token
@@ -149,7 +149,7 @@ module type GrammarSig = sig
   val action : 'a -> action
   val entry_create : string -> 'a entry
   val entry_parse : 'a entry -> parsable -> 'a
-  val entry_print : 'a entry -> unit
+  val entry_print : Format.formatter -> 'a entry -> unit
   val srules' : production_rule list -> symbol
 end
 
@@ -162,7 +162,7 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
   let action = Action.mk
   let entry_create = Entry.mk
   let entry_parse e s = parse e (*FIXME*)Loc.ghost s
-  let entry_print x = Entry.print !Pp_control.std_ft x
+  let entry_print ft x = Entry.print ft x
   let srules' = srules (entry_create "dummy")
 end
 
diff --git a/lib/pp.mli b/lib/pp.mli
index 135343092d..8b3f6ff244 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -103,7 +103,6 @@ val pp : std_ppcmds -> unit
 val ppnl : std_ppcmds -> unit
 val pperr : std_ppcmds -> unit
 val pperrnl : std_ppcmds -> unit
-val message : string -> unit       (** = pPNL *)
 val pp_flush : unit -> unit
 val flush_all: unit -> unit
 
@@ -122,6 +121,7 @@ val msg : std_ppcmds -> unit
 val msgnl : std_ppcmds -> unit
 val msgerr : std_ppcmds -> unit
 val msgerrnl : std_ppcmds -> unit
+val message : string -> unit       (** = pPNL *)
 
 (** {6 Location management. } *)
 
diff --git a/lib/system.ml b/lib/system.ml
index 1537f48927..238efcff75 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -105,8 +105,8 @@ let open_trapping_failure name =
 
 let try_remove filename =
   try Sys.remove filename
-  with _ -> msgnl (str"Warning: " ++ str"Could not remove file " ++
-                   str filename ++ str" which is corrupted!" )
+  with _ -> msg_warning
+    (str"Could not remove file " ++ str filename ++ str" which is corrupted!")
 
 let marshal_out ch v = Marshal.to_channel ch v []
 let marshal_in ch =