deprecate Pp.std_ppcmds type alias

7 files changed, 21 insertions, 23 deletions

diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index 306ff1868..edbb7c6b7 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -40,7 +40,7 @@ val auto_multi_rewrite : ?conds:conditions -> string list -> Locus.clause -> uni
 
 val auto_multi_rewrite_with : ?conds:conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic
 
-val print_rewrite_hintdb : string -> Pp.std_ppcmds
+val print_rewrite_hintdb : string -> Pp.t
 
 open Clenv
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 6cc9d3d55..72e57a85b 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -621,7 +621,7 @@ module V85 = struct
 
   type autoinfo = { hints : hint_db; is_evar: existential_key option;
                     only_classes: bool; unique : bool;
-                    auto_depth: int list; auto_last_tac: std_ppcmds Lazy.t;
+                    auto_depth: int list; auto_last_tac: Pp.t Lazy.t;
                     auto_path : global_reference option list;
                     auto_cut : hints_path }
   type autogoal = goal * autoinfo
@@ -972,7 +972,7 @@ end
 module Search = struct
   type autoinfo =
     { search_depth : int list;
-      last_tac : Pp.std_ppcmds Lazy.t;
+      last_tac : Pp.t Lazy.t;
       search_dep : bool;
       search_only_classes : bool;
       search_cut : hints_path;
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 64d4d3135..65864bd47 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -203,7 +203,7 @@ type search_state = {
   priority : int;
   depth : int; (*r depth of search before failing *)
   tacres : goal list sigma;
-  last_tactic : std_ppcmds Lazy.t;
+  last_tactic : Pp.t Lazy.t;
   dblist : hint_db list;
   localdb :  hint_db list;
   prev : prev_search_state;
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 6325a4470..44e5370e9 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Util
 open Names
 open EConstr
@@ -85,10 +84,10 @@ type hints_path = global_reference hints_path_gen
 val normalize_path : hints_path -> hints_path
 val path_matches : hints_path -> hints_path_atom list -> bool
 val path_derivate : hints_path -> hints_path_atom -> hints_path
-val pp_hints_path_gen : ('a -> Pp.std_ppcmds) -> 'a hints_path_gen -> Pp.std_ppcmds
-val pp_hints_path_atom : ('a -> Pp.std_ppcmds) -> 'a hints_path_atom_gen -> Pp.std_ppcmds
-val pp_hints_path : hints_path -> Pp.std_ppcmds
-val pp_hint_mode : hint_mode -> Pp.std_ppcmds
+val pp_hints_path_gen : ('a -> Pp.t) -> 'a hints_path_gen -> Pp.t
+val pp_hints_path_atom : ('a -> Pp.t) -> 'a hints_path_atom_gen -> Pp.t
+val pp_hints_path : hints_path -> Pp.t
+val pp_hint_mode : hint_mode -> Pp.t
 val glob_hints_path_atom :
   Libnames.reference hints_path_atom_gen -> Globnames.global_reference hints_path_atom_gen
 val glob_hints_path :
@@ -261,12 +260,12 @@ val rewrite_db : hint_db_name
 
 (** Printing  hints *)
 
-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
-val pr_hint : hint -> Pp.std_ppcmds
+val pr_searchtable : unit -> Pp.t
+val pr_applicable_hint : unit -> Pp.t
+val pr_hint_ref : global_reference -> Pp.t
+val pr_hint_db_by_name : hint_db_name -> Pp.t
+val pr_hint_db : Hint_db.t -> Pp.t
+val pr_hint : hint -> Pp.t
 
 (** Hook for changing the initialization of auto *)
 
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli
index 005555caa..f825c4f4a 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -48,4 +48,4 @@ val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant
 val check_scheme : 'a scheme_kind -> inductive -> bool
 
 
-val pr_scheme_kind : 'a scheme_kind -> Pp.std_ppcmds
+val pr_scheme_kind : 'a scheme_kind -> Pp.t
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 4ad9c6541..2a04c413b 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Names
 open Term
 open EConstr
@@ -19,7 +18,7 @@ open Tactypes
 (** Tacticals i.e. functions from tactics to tactics. *)
 
 val tclIDTAC         : tactic
-val tclIDTAC_MESSAGE : std_ppcmds -> tactic
+val tclIDTAC_MESSAGE : Pp.t -> tactic
 val tclORELSE0       : tactic -> tactic -> tactic
 val tclORELSE        : tactic -> tactic -> tactic
 val tclTHEN          : tactic -> tactic -> tactic
@@ -41,8 +40,8 @@ val tclSOLVE         : tactic list -> tactic
 val tclTRY           : tactic -> tactic
 val tclCOMPLETE      : tactic -> tactic
 val tclAT_LEAST_ONCE : tactic -> tactic
-val tclFAIL          : int -> std_ppcmds -> tactic
-val tclFAIL_lazy     : int -> std_ppcmds Lazy.t -> tactic
+val tclFAIL          : int -> Pp.t -> tactic
+val tclFAIL_lazy     : int -> Pp.t Lazy.t -> tactic
 val tclDO            : int -> tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclSHOWHYPS      : tactic -> tactic
@@ -160,9 +159,9 @@ module New : sig
   (* [tclFAIL n msg] fails with [msg] as an error message at level [n]
      (meaning that it will jump over [n] error catching tacticals FROM
      THIS MODULE. *)
-  val tclFAIL : int -> Pp.std_ppcmds -> 'a tactic
+  val tclFAIL : int -> Pp.t -> 'a tactic
 
-  val tclZEROMSG : ?loc:Loc.t -> Pp.std_ppcmds -> 'a tactic
+  val tclZEROMSG : ?loc:Loc.t -> Pp.t -> 'a tactic
   (** Fail with a [User_Error] containing the given message. *)
 
   val tclOR : unit tactic -> unit tactic -> unit tactic
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index e90e1959e..64ba38a51 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -49,7 +49,7 @@ struct
     | DNil
 
   (* debug *)
-  let _pr_dconstr f : 'a t -> std_ppcmds = function
+  let _pr_dconstr f : 'a t -> Pp.t = function
     | DRel -> str "*"
     | DSort -> str "Sort"
     | DRef _ -> str "Ref"