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, 6 insertions, 9 deletions

diff --git a/tactics/auto.mli b/tactics/auto.mli
index 67e4dac97..792900984 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;