deprecate Pp.std_ppcmds type alias

10 files changed, 35 insertions, 36 deletions

diff --git a/engine/geninterp.ml b/engine/geninterp.ml
index 9964433a8..e79e258fb 100644
--- a/engine/geninterp.ml
+++ b/engine/geninterp.ml
@@ -32,7 +32,7 @@ struct
   let repr = ValT.repr
   let create = ValT.create
 
-  let pr : type a. a typ -> Pp.std_ppcmds = fun t -> Pp.str (repr t)
+  let pr : type a. a typ -> Pp.t = fun t -> Pp.str (repr t)
 
   let typ_list = ValT.create "list"
   let typ_opt = ValT.create "option"
diff --git a/engine/geninterp.mli b/engine/geninterp.mli
index 9a925dcd8..492e372ad 100644
--- a/engine/geninterp.mli
+++ b/engine/geninterp.mli
@@ -30,7 +30,7 @@ sig
 
   val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option
   val repr : 'a typ -> string
-  val pr : 'a typ -> Pp.std_ppcmds
+  val pr : 'a typ -> Pp.t
 
   val typ_list : t list typ
   val typ_opt : t option typ
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index aaebe4c1b..8c8f9fe93 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -57,11 +57,11 @@ module NonLogical : sig
   val print_char : char -> unit t
 
   (** Loggers. The buffer is also flushed. *)
-  val print_debug : Pp.std_ppcmds -> unit t
-  val print_warning : Pp.std_ppcmds -> unit t
-  val print_notice : Pp.std_ppcmds -> unit t
-  val print_info : Pp.std_ppcmds -> unit t
-  val print_error : Pp.std_ppcmds -> unit t
+  val print_debug : Pp.t -> unit t
+  val print_warning : Pp.t -> unit t
+  val print_notice : Pp.t -> unit t
+  val print_info : Pp.t -> unit t
+  val print_error : Pp.t -> unit t
 
   (** [Pervasives.raise]. Except that exceptions are wrapped with
       {!Exception}. *)
diff --git a/engine/proofview.ml b/engine/proofview.ml
index b4e2160f4..eef2b83f4 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -332,7 +332,7 @@ exception NoSuchGoals of int
 (* This hook returns a string to be appended to the usual message.
    Primarily used to add a suggestion about the right bullet to use to
    focus the next goal, if applicable. *)
-let nosuchgoals_hook:(int -> std_ppcmds) ref = ref (fun n -> mt ())
+let nosuchgoals_hook:(int -> Pp.t) ref = ref (fun n -> mt ())
 let set_nosuchgoals_hook f = nosuchgoals_hook := f
 
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 957c9213c..d92d0a7d5 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -235,7 +235,7 @@ val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic
     This hook is used to add a suggestion about bullets when
     applicable. *)
 exception NoSuchGoals of int
-val set_nosuchgoals_hook: (int -> Pp.std_ppcmds) -> unit
+val set_nosuchgoals_hook: (int -> Pp.t) -> unit
 
 val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
 
@@ -526,7 +526,7 @@ module Trace : sig
   val log : Proofview_monad.lazy_msg -> unit tactic
   val name_tactic : Proofview_monad.lazy_msg -> 'a tactic -> 'a tactic
 
-  val pr_info : ?lvl:int -> Proofview_monad.Info.tree -> Pp.std_ppcmds
+  val pr_info : ?lvl:int -> Proofview_monad.Info.tree -> Pp.t
 
 end
 
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 1b737b6f4..d0f471225 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -62,7 +62,7 @@ end
 
 (** We typically label nodes of [Trace.tree] with messages to
     print. But we don't want to compute the result. *)
-type lazy_msg = unit -> Pp.std_ppcmds
+type lazy_msg = unit -> Pp.t
 let pr_lazy_msg msg = msg ()
 
 (** Info trace. *)
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index 554583421..e7123218b 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -43,7 +43,7 @@ end
 
 (** We typically label nodes of [Trace.tree] with messages to
     print. But we don't want to compute the result. *)
-type lazy_msg = unit -> Pp.std_ppcmds
+type lazy_msg = unit -> Pp.t
 
 (** Info trace. *)
 module Info : sig
@@ -58,7 +58,7 @@ module Info : sig
   type state = tag Trace.incr
   type tree = tag Trace.forest
 
-  val print : tree -> Pp.std_ppcmds
+  val print : tree -> Pp.t
 
   (** [collapse n t] flattens the first [n] levels of [Tactic] in an
       info trace, effectively forgetting about the [n] top level of
diff --git a/engine/termops.mli b/engine/termops.mli
index c19a2d15a..2624afd30 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -9,16 +9,15 @@
 (** This file defines various utilities for term manipulation that are not
     needed in the kernel. *)
 
-open Pp
 open Names
 open Term
 open Environ
 open EConstr
 
 (** printers *)
-val print_sort : sorts -> std_ppcmds
-val pr_sort_family : sorts_family -> std_ppcmds
-val pr_fix : ('a -> std_ppcmds) -> ('a, 'a) pfixpoint -> std_ppcmds
+val print_sort : sorts -> Pp.t
+val pr_sort_family : sorts_family -> Pp.t
+val pr_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t
 
 (** about contexts *)
 val push_rel_assum : Name.t * types -> env -> env
@@ -279,25 +278,25 @@ val on_judgment_type  : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) puns
 
 open Evd
 
-val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds
+val pr_existential_key : evar_map -> evar -> Pp.t
 
 val pr_evar_suggested_name : existential_key -> evar_map -> Id.t
 
-val pr_evar_info : evar_info -> Pp.std_ppcmds
-val pr_evar_constraints : evar_map -> evar_constraint list -> Pp.std_ppcmds
-val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds
+val pr_evar_info : evar_info -> Pp.t
+val pr_evar_constraints : evar_map -> evar_constraint list -> Pp.t
+val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.t
 val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) ->
-  evar_map -> Pp.std_ppcmds
-val pr_metaset : Metaset.t -> Pp.std_ppcmds
-val pr_evar_universe_context : evar_universe_context -> Pp.std_ppcmds
-val pr_evd_level : evar_map -> Univ.Level.t -> Pp.std_ppcmds
+  evar_map -> Pp.t
+val pr_metaset : Metaset.t -> Pp.t
+val pr_evar_universe_context : evar_universe_context -> Pp.t
+val pr_evd_level : evar_map -> Univ.Level.t -> Pp.t
 
 (** debug printer: do not use to display terms to the casual user... *)
 
-val set_print_constr : (env -> Evd.evar_map -> constr -> std_ppcmds) -> unit
-val print_constr     : constr -> std_ppcmds
-val print_constr_env : env -> Evd.evar_map -> constr -> std_ppcmds
-val print_named_context : env -> std_ppcmds
-val pr_rel_decl : env -> Context.Rel.Declaration.t -> std_ppcmds
-val print_rel_context : env -> std_ppcmds
-val print_env : env -> std_ppcmds
+val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit
+val print_constr     : constr -> Pp.t
+val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t
+val print_named_context : env -> Pp.t
+val pr_rel_decl : env -> Context.Rel.Declaration.t -> Pp.t
+val print_rel_context : env -> Pp.t
+val print_env : env -> Pp.t
diff --git a/engine/uState.mli b/engine/uState.mli
index 3776e4c9f..d198fbfbe 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -123,4 +123,4 @@ val update_sigma_env : t -> Environ.env -> t
 
 (** {5 Pretty-printing} *)
 
-val pr_uctx_level : t -> Univ.Level.t -> Pp.std_ppcmds
+val pr_uctx_level : t -> Univ.Level.t -> Pp.t
diff --git a/engine/universes.mli b/engine/universes.mli
index 0f6e419d0..fe40f8238 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -17,7 +17,7 @@ val is_set_minimization : unit -> bool
 
 (** Universes *)
 
-val pr_with_global_universes : Level.t -> Pp.std_ppcmds
+val pr_with_global_universes : Level.t -> Pp.t
 
 (** Local universe name <-> level mapping *)
 
@@ -52,7 +52,7 @@ type universe_constraint = universe * universe_constraint_type * universe
 module Constraints : sig
   include Set.S with type elt = universe_constraint
 		       
-  val pr : t -> Pp.std_ppcmds
+  val pr : t -> Pp.t
 end
 
 type universe_constraints = Constraints.t
@@ -203,7 +203,7 @@ val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_s
 
 (** Pretty-printing *)
 
-val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds
+val pr_universe_opt_subst : universe_opt_subst -> Pp.t
 
 (** {6 Support for template polymorphism } *)