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, 35 insertions, 38 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 699f1f3dfd..6fda2284a8 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -23,8 +23,8 @@ let init_size=5
 
 let cc_verbose=ref false
 
-let debug f x =
-  if !cc_verbose then f x
+let debug x =
+  if !cc_verbose then msg_debug x
 
 let _=
   let gdopt=
@@ -512,7 +512,7 @@ let add_inst state (inst,int_subst) =
   check_for_interrupt ();
   if state.rew_depth > 0 then
   if is_redundant state inst.qe_hyp_id int_subst then
-    debug msgnl (str "discarding redundant (dis)equality")
+    debug (str "discarding redundant (dis)equality")
   else
     begin
       Identhash.add state.q_history inst.qe_hyp_id int_subst;
@@ -527,20 +527,18 @@ let add_inst state (inst,int_subst) =
 	    state.rew_depth<-pred state.rew_depth;
 	    if inst.qe_pol then
 	      begin
-		debug (fun () ->
-		  msgnl
-		   (str "Adding new equality, depth="++ int state.rew_depth);
-	          msgnl (str "  [" ++ Termops.print_constr prf ++ str " : " ++
-			   pr_term s ++ str " == " ++ pr_term t ++ str "]")) ();
+		debug (
+		   (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
+	          (str "  [" ++ Termops.print_constr prf ++ str " : " ++
+			   pr_term s ++ str " == " ++ pr_term t ++ str "]"));
 		add_equality state prf s t
 	      end
 	    else
 	      begin
-		debug (fun () ->
-		  msgnl
-		   (str "Adding new disequality, depth="++ int state.rew_depth);
-	          msgnl (str "  [" ++ Termops.print_constr prf ++ str " : " ++
-			   pr_term s ++ str " <> " ++ pr_term t ++ str "]")) ();
+		debug (
+		   (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
+	          (str "  [" ++ Termops.print_constr prf ++ str " : " ++
+			   pr_term s ++ str " <> " ++ pr_term t ++ str "]"));
 		add_disequality state (Hyp prf) s t
 	      end
   end
@@ -566,8 +564,8 @@ let join_path uf i j=
   min_path (down_path uf i [],down_path uf j [])
 
 let union state i1 i2 eq=
-  debug (fun () -> msgnl (str "Linking " ++ pr_idx_term state i1 ++
-		 str " and " ++ pr_idx_term state i2 ++ str ".")) ();
+  debug (str "Linking " ++ pr_idx_term state i1 ++
+		 str " and " ++ pr_idx_term state i2 ++ str ".");
   let r1= get_representative state.uf i1
   and r2= get_representative state.uf i2 in
     link state.uf i1 i2 eq;
@@ -606,9 +604,9 @@ let union state i1 i2 eq=
 	| _,_ -> ()
 
 let merge eq state = (* merge and no-merge *)
-  debug (fun () -> msgnl
+  debug
     (str "Merging " ++ pr_idx_term state eq.lhs ++
-       str " and " ++ pr_idx_term state eq.rhs ++ str ".")) ();
+       str " and " ++ pr_idx_term state eq.rhs ++ str ".");
   let uf=state.uf in
   let i=find uf eq.lhs
   and j=find uf eq.rhs in
@@ -619,8 +617,8 @@ let merge eq state = (* merge and no-merge *)
 	union state j i (swap eq)
 
 let update t state = (* update 1 and 2 *)
-  debug (fun () -> msgnl
-    (str "Updating term " ++ pr_idx_term state t ++ str ".")) ();
+  debug
+    (str "Updating term " ++ pr_idx_term state t ++ str ".");
   let (i,j) as sign = signature state.uf t in
   let (u,v) = subterms state.uf t in
   let rep = get_representative state.uf i in
@@ -680,8 +678,8 @@ let process_constructor_mark t i rep pac state =
 	    end
 
 let process_mark t m state =
-  debug (fun () -> msgnl
-    (str "Processing mark for term " ++ pr_idx_term state t ++ str ".")) ();
+  debug
+    (str "Processing mark for term " ++ pr_idx_term state t ++ str ".");
   let i=find state.uf t in
   let rep=get_representative state.uf i in
     match m with
@@ -701,9 +699,9 @@ let check_disequalities state =
           if find uf dis.lhs = find uf dis.rhs then (str "Yes", Some dis)
           else (str "No", check_aux q)
         in
-        let _ = debug (fun () -> msg_debug
+        let _ = debug
         (str "Checking if " ++ pr_idx_term state dis.lhs ++ str " = " ++
-         pr_idx_term state dis.rhs ++ str " ... " ++ info)) () in
+         pr_idx_term state dis.rhs ++ str " ... " ++ info) in
         ans
     | [] -> None
   in
@@ -889,7 +887,7 @@ let find_instances state =
   let pb_stack= init_pb_stack state in
   let res =ref [] in
   let _ =
-    debug msgnl (str "Running E-matching algorithm ... ");
+    debug (str "Running E-matching algorithm ... ");
     try
       while true do
 	check_for_interrupt ();
@@ -900,7 +898,7 @@ let find_instances state =
     !res
 
 let rec execute first_run state =
-  debug msgnl (str "Executing ... ");
+  debug (str "Executing ... ");
   try
     while
       check_for_interrupt ();
@@ -910,7 +908,7 @@ let rec execute first_run state =
 	None ->
 	  if not(Intset.is_empty state.pa_classes) then
 	    begin
-	      debug msgnl (str "First run was incomplete, completing ... ");
+	      debug (str "First run was incomplete, completing ... ");
 	      complete state;
 	      execute false state
 	    end
@@ -925,12 +923,12 @@ let rec execute first_run state =
 		  end
 		else
 	      begin
-		debug msgnl (str "Out of instances ... ");
+		debug (str "Out of instances ... ");
 		None
 	      end
 	    else
 	      begin
-		debug msgnl (str "Out of depth ... ");
+		debug (str "Out of depth ... ");
 		None
 	      end
       | Some dis -> Some
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 78dbee3fe8..2d017f5cfe 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -71,7 +71,7 @@ module Termhash : Hashtbl.S with type key = term
 
 val constr_of_term : term -> constr
 
-val debug : (Pp.std_ppcmds -> unit) -> Pp.std_ppcmds -> unit
+val debug : Pp.std_ppcmds -> unit
 
 val forest : state -> forest
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7940009c6e..204af93d56 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -378,16 +378,16 @@ let build_term_to_complete uf meta pac =
 
 let cc_tactic depth additionnal_terms gls=
   Coqlib.check_required_library ["Coq";"Init";"Logic"];
-  let _ = debug Pp.msgnl (Pp.str "Reading subgoal ...") in
+  let _ = debug (Pp.str "Reading subgoal ...") in
   let state = make_prb gls depth additionnal_terms in
-  let _ = debug Pp.msgnl (Pp.str "Problem built, solving ...") in
+  let _ = debug (Pp.str "Problem built, solving ...") in
   let sol = execute true state in
-  let _ = debug Pp.msgnl (Pp.str "Computation completed.") in
+  let _ = debug (Pp.str "Computation completed.") in
   let uf=forest state in
     match sol with
 	None -> tclFAIL 0 (str "congruence failed") gls
       | Some reason ->
-	  debug Pp.msgnl (Pp.str "Goal solved, generating proof ...");
+	  debug (Pp.str "Goal solved, generating proof ...");
 	  match reason with
 	      Discrimination (i,ipac,j,jpac) ->
 		let p=build_proof uf (`Discr (i,ipac,j,jpac)) in
@@ -400,10 +400,10 @@ let cc_tactic depth additionnal_terms gls=
 		  List.map
 		    (build_term_to_complete uf newmeta)
 		    (epsilons uf) in
-		  Pp.msgnl
+		  Pp.msg_info
 		    (Pp.str "Goal is solvable by congruence but \
  some arguments are missing.");
-		  Pp.msgnl
+		  Pp.msg_info
 		    (Pp.str "  Try " ++
 		     hov 8
 		       begin
@@ -413,9 +413,8 @@ let cc_tactic depth additionnal_terms gls=
 			   (Termops.print_constr_env (pf_env gls))
 			   terms_to_complete ++
 			 str ")\","
-		       end);
-		  Pp.msgnl
-		    (Pp.str "  replacing metavariables by arbitrary terms.");
+		       end ++
+		    Pp.str "  replacing metavariables by arbitrary terms.");
 		  tclFAIL 0 (str "Incomplete") gls
 	    | Contradiction dis ->
 		let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in