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

6 files changed, 16 insertions, 20 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 046b65ee8f..bd5fd9c09c 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -18,7 +18,7 @@ open Libnames
 open Globnames
 open Misctypes
 
-let msgnl = Pp.msgnl
+(* let msgnl = Pp.msgnl *)
 
 (*
 let observe strm =
@@ -60,17 +60,17 @@ let rec print_debug_queue b e =
     begin
       let lmsg,goal = Stack.pop debug_queue in 
       if b then 
-	Pp.msgnl (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
+	Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
       else
 	begin
-	  Pp.msgnl (str " from " ++ lmsg ++ str " on goal " ++ goal);
+	  Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal);
 	end;
       print_debug_queue false e;
     end
 
 let observe strm =
   if do_observe ()
-  then Pp.msgnl strm
+  then Pp.msg_debug strm
   else ()
 
 let do_observe_tac s tac g = 
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 21f77e438d..42e5c36a8c 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -36,7 +36,7 @@ let pr_elim_scheme el =
 
 let observe s =
   if do_observe ()
-  then Pp.msgnl s
+  then Pp.msg_debug s
 
 
 let pr_elim_scheme el =
@@ -54,7 +54,7 @@ let pr_elim_scheme el =
 
 let observe s =
   if do_observe ()
-  then Pp.msgnl s
+  then Pp.msg_debug s
 
 (*
    Transform an inductive induction principle into
@@ -394,9 +394,7 @@ let generate_functional_principle
 	     Decl_kinds.IsDefinition (Decl_kinds.Scheme)
 	    )
 	);
-	Flags.if_verbose
-	  (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined"))
-	  name;
+	Declare.definition_message name;
 	names := name :: !names
       in
       register_with_sort InProp;
@@ -676,8 +674,7 @@ let build_scheme fas =
 	 (Declare.declare_constant
 	    princ_id
 	    (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
-       Flags.if_verbose
-	 (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) princ_id
+       Declare.definition_message princ_id
     )
     fas
     bodies_types;
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index a169c28260..7b341e581b 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -14,7 +14,7 @@ open Misctypes
 
 let observe strm =
   if do_observe ()
-  then Pp.msgnl strm
+  then Pp.msg_debug strm
   else ()
 (*let observennl strm =
   if do_observe ()
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 026b9ad0ec..8443959b4b 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -153,9 +153,8 @@ open Declarations
 open Entries
 open Decl_kinds
 open Declare
-let definition_message id =
-  Flags.if_verbose message ((string_of_id id) ^ " is defined")
 
+let definition_message = Declare.definition_message
 
 let save with_clean id const (locality,kind) hook =
   let {const_entry_body = pft;
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b463b6c27b..7745996c58 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -48,11 +48,11 @@ let pr_constr_with_binding prc (c,bl) :  Pp.std_ppcmds =
   pr_with_bindings prc prc  (c,bl)
 
 (* The local debuging mechanism *)
-let msgnl = Pp.msgnl
+(* let msgnl = Pp.msgnl *)
 
 let observe strm =
   if do_observe ()
-  then Pp.msgnl strm
+  then Pp.msg_debug strm
   else ()
 
 (*let observennl strm =
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5fcd495ef9..7cf438e6f5 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -235,17 +235,17 @@ let rec print_debug_queue b e =
     begin
       let lmsg,goal = Stack.pop debug_queue in 
       if b then 
-	Pp.msgnl (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
+	Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
       else
 	begin
-	  Pp.msgnl (str " from " ++ lmsg ++ str " on goal " ++ goal);
+	  Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal);
 	end;
       print_debug_queue false e;
     end
 
 let observe strm =
   if do_observe ()
-  then Pp.msgnl strm
+  then Pp.msg_debug strm
   else ()
 
 
@@ -413,7 +413,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
 	    (fun g' -> 
 	      let ty_teq = pf_type_of g' (mkVar heq) in
 	      let teq_lhs,teq_rhs =
-		let _,args = try destApp ty_teq with _ -> Pp.msgnl (Printer.pr_goal g' ++ fnl () ++ pr_id heq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false in
+		let _,args = try destApp ty_teq with _ -> assert false in
 		args.(1),args.(2)
 	      in
 	      let new_b' = Termops.replace_term teq_lhs teq_rhs new_b in