Getting rid of Pp.msg

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

4 files changed, 42 insertions, 46 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 404516279a..96cef72b44 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -411,6 +411,10 @@ module Hint_db = struct
     f None (List.map (fun x -> snd (snd x)) db.hintdb_nopat);
     Constr_map.iter (fun k (l,l',_) -> f (Some k) (List.map snd (l@l'))) db.hintdb_map
 
+  let fold f db accu =
+    let accu = f None (List.map (fun x -> snd (snd x)) db.hintdb_nopat) accu in
+    Constr_map.fold (fun k (l,l',_) -> f (Some k) (List.map snd (l@l'))) db.hintdb_map accu
+
   let transparent_state db = db.hintdb_state
 
   let set_transparent_state db st =
@@ -921,7 +925,6 @@ let pr_hint_list_for_head c =
 let pr_hint_ref ref = pr_hint_list_for_head ref
 
 (* Print all hints associated to head id in any database *)
-let print_hint_ref ref =  ppnl(pr_hint_ref ref)
 
 let pr_hint_term cl =
   try
@@ -949,53 +952,51 @@ let pr_hint_term cl =
 let error_no_such_hint_database x =
   error ("No such Hint database: "^x^".")
 
-let print_hint_term cl = ppnl (pr_hint_term cl)
-
 (* print all hints that apply to the concl of the current goal *)
-let print_applicable_hint () =
+let pr_applicable_hint () =
   let pts = get_pftreestate () in
   let glss = Proof.V82.subgoals pts in
   match glss.Evd.it with
   | [] -> Errors.error "No focused goal."
   | g::_ ->
     let gl = { Evd.it = g; sigma = glss.Evd.sigma } in
-    print_hint_term (pf_concl gl)
+    pr_hint_term (pf_concl gl)
 
 (* displays the whole hint database db *)
-let print_hint_db db =
+let pr_hint_db db =
+  let content =
+    let fold head hintlist accu =
+      let goal_descr = match head with
+      | None -> str "For any goal"
+      | Some head -> str "For " ++ pr_global head
+      in
+      let hints = pr_hint_list (List.map (fun x -> (0, x)) hintlist) in
+      let hint_descr = hov 0 (goal_descr ++ str " -> " ++ hints) in
+      accu ++ hint_descr
+    in
+    Hint_db.fold fold db (mt ())
+  in
   let (ids, csts) = Hint_db.transparent_state db in
-  msgnl (hov 0
-	  ((if Hint_db.use_dn db then str"Discriminated database"
-	    else str"Non-discriminated database")));
-  msgnl (hov 2 (str"Unfoldable variable definitions: " ++ pr_idpred ids));
-  msgnl (hov 2 (str"Unfoldable constant definitions: " ++ pr_cpred csts));
-  msgnl (hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)));
-  Hint_db.iter
-    (fun head hintlist ->
-      match head with
-      | Some head ->
-	  msg (hov 0
-		  (str "For " ++ pr_global head ++ str " -> " ++
-		      pr_hint_list (List.map (fun x -> (0,x)) hintlist)))
-      | None ->
-	  msg (hov 0
-		  (str "For any goal -> " ++
-		      pr_hint_list (List.map (fun x -> (0, x)) hintlist))))
-    db
-
-let print_hint_db_by_name dbname =
+  hov 0
+    ((if Hint_db.use_dn db then str"Discriminated database"
+      else str"Non-discriminated database")) ++ fnl () ++
+  hov 2 (str"Unfoldable variable definitions: " ++ pr_idpred ids) ++ fnl () ++
+  hov 2 (str"Unfoldable constant definitions: " ++ pr_cpred csts) ++ fnl () ++
+  hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)) ++ fnl () ++
+  content
+
+let pr_hint_db_by_name dbname =
   try
-    let db = searchtable_map dbname in print_hint_db db
+    let db = searchtable_map dbname in pr_hint_db db
   with Not_found ->
     error_no_such_hint_database dbname
 
 (* displays all the hints of all databases *)
-let print_searchtable () =
-  Hintdbmap.iter
-    (fun name db ->
-       msg (str "In the database " ++ str name ++ str ":" ++ fnl ());
-       print_hint_db db)
-    !searchtable
+let pr_searchtable () =
+  let fold name db accu =
+    str "In the database " ++ str name ++ str ":" ++ fnl () ++ pr_hint_db db
+  in
+  Hintdbmap.fold fold !searchtable (mt ())
 
 (**************************************************************************)
 (*                           Automatic tactics                            *)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 67e4dac97e..792900984e 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -19,6 +19,7 @@ open Globnames
 open Vernacexpr
 open Mod_subst
 open Misctypes
+open Pp
 
 (** Auto and related automation tactics *)
 
@@ -124,15 +125,11 @@ val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit
 
 val prepare_hint : env -> open_constr -> constr
 
-val print_searchtable : unit -> unit
-
-val print_applicable_hint : unit -> unit
-
-val print_hint_ref : global_reference -> unit
-
-val print_hint_db_by_name : hint_db_name -> unit
-
-val print_hint_db : Hint_db.t -> unit
+val pr_searchtable : unit -> std_ppcmds
+val pr_applicable_hint : unit -> std_ppcmds
+val pr_hint_ref : global_reference -> std_ppcmds
+val pr_hint_db_by_name : hint_db_name -> std_ppcmds
+val pr_hint_db : Hint_db.t -> std_ppcmds
 
 (** [make_exact_entry pri (c, ctyp)].
    [c] is the term given as an exact proof to solve the goal;
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 82b08289da..cdb192ffa9 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -779,6 +779,5 @@ END
 VERNAC COMMAND EXTEND GrabEvars
 [ "Grab" "Existential" "Variables" ] ->
   [ let p = Proof_global.give_me_the_proof () in
-    Proof.V82.grab_evars p;
-    Flags.if_verbose (fun () -> Pp.msg (Printer.pr_open_subgoals ())) () ]
+    Proof.V82.grab_evars p ]
 END
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 16eb595eaf..665ab5b393 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1742,8 +1742,7 @@ let add_morphism_infer glob m n =
 				   glob (ConstRef cst));
 		  declare_projection n instance_id (ConstRef cst)
 		| _ -> assert false);
-	    Pfedit.by (Tacinterp.interp <:tactic< Coq.Classes.SetoidTactics.add_morphism_tactic>>)) ();
-	Flags.if_verbose (fun x -> msg (Printer.pr_open_subgoals x)) ()
+	    Pfedit.by (Tacinterp.interp <:tactic< Coq.Classes.SetoidTactics.add_morphism_tactic>>)) ()
 
 let add_morphism glob binders m s n =
   init_setoid ();