deprecate Pp.std_ppcmds type alias

21 files changed, 132 insertions, 137 deletions

diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index e6abf1ccf..f904aa3e6 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -120,7 +120,7 @@ val term_equal : term -> term -> bool
 
 val constr_of_term : term -> constr
 
-val debug : (unit -> Pp.std_ppcmds) -> unit
+val debug : (unit -> Pp.t) -> unit
 
 val forest : state -> forest
 
@@ -169,7 +169,7 @@ val find_instances : state -> (quant_eq * int array) list
 
 val execute : bool -> state -> explanation option
 
-val pr_idx_term : forest -> int -> Pp.std_ppcmds
+val pr_idx_term : forest -> int -> Pp.t
 
 val empty_forest: unit -> forest
 
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index d6342b59c..356bad98b 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -9,30 +9,29 @@
 open Names
 open Globnames
 open Miniml
-open Pp
 
 (** By default, in module Format, you can do horizontal placing of blocks
     even if they include newlines, as long as the number of chars in the
     blocks are less that a line length. To avoid this awkward situation,
     we attach a big virtual size to [fnl] newlines. *)
 
-val fnl : unit -> std_ppcmds
-val fnl2 : unit -> std_ppcmds
-val space_if : bool -> std_ppcmds
+val fnl : unit -> Pp.t
+val fnl2 : unit -> Pp.t
+val space_if : bool -> Pp.t
 
-val pp_par : bool -> std_ppcmds -> std_ppcmds
+val pp_par : bool -> Pp.t -> Pp.t
 
 (** [pp_apply] : a head part applied to arguments, possibly with parenthesis *)
-val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds
+val pp_apply : Pp.t -> bool -> Pp.t list -> Pp.t
 
 (** Same as [pp_apply], but with also protection of the head by parenthesis *)
-val pp_apply2 : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds
+val pp_apply2 : Pp.t -> bool -> Pp.t list -> Pp.t
 
-val pp_tuple_light : (bool -> 'a -> std_ppcmds) -> 'a list -> std_ppcmds
-val pp_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
-val pp_boxed_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+val pp_tuple_light : (bool -> 'a -> Pp.t) -> 'a list -> Pp.t
+val pp_tuple : ('a -> Pp.t) -> 'a list -> Pp.t
+val pp_boxed_tuple : ('a -> Pp.t) -> 'a list -> Pp.t
 
-val pr_binding : Id.t list -> std_ppcmds
+val pr_binding : Id.t list -> Pp.t
 
 val rename_id : Id.t -> Id.Set.t -> Id.t
 
@@ -80,4 +79,4 @@ val mk_ind : string -> string -> MutInd.t
 
 val is_native_char : ml_ast -> bool
 val get_native_char : ml_ast -> char
-val pp_native_char : ml_ast -> std_ppcmds
+val pp_native_char : ml_ast -> Pp.t
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index e10dcd48b..5769ff117 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -29,7 +29,7 @@ val mono_environment :
 (* Used by the Relation Extraction plugin *)
 
 val print_one_decl :
-  Miniml.ml_structure -> ModPath.t -> Miniml.ml_decl -> Pp.std_ppcmds
+  Miniml.ml_structure -> ModPath.t -> Miniml.ml_decl -> Pp.t
 
 (* Used by Extraction Compute *)
 
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index be8282da0..edebba49d 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -8,7 +8,6 @@
 
 (*s Target language for extraction: a core ML called MiniML. *)
 
-open Pp
 open Names
 open Globnames
 
@@ -205,19 +204,19 @@ type language_descr = {
   file_naming : ModPath.t -> string;
   (* the second argument is a comment to add to the preamble *)
   preamble :
-    Id.t -> std_ppcmds option -> ModPath.t list -> unsafe_needs ->
-    std_ppcmds;
-  pp_struct : ml_structure -> std_ppcmds;
+    Id.t -> Pp.t option -> ModPath.t list -> unsafe_needs ->
+    Pp.t;
+  pp_struct : ml_structure -> Pp.t;
 
   (* Concerning a possible interface file *)
   sig_suffix : string option;
   (* the second argument is a comment to add to the preamble *)
   sig_preamble :
-    Id.t -> std_ppcmds option -> ModPath.t list -> unsafe_needs ->
-    std_ppcmds;
-  pp_sig : ml_signature -> std_ppcmds;
+    Id.t -> Pp.t option -> ModPath.t list -> unsafe_needs ->
+    Pp.t;
+  pp_sig : ml_signature -> Pp.t;
 
   (* for an isolated declaration print *)
-  pp_decl : ml_decl -> std_ppcmds;
+  pp_decl : ml_decl -> Pp.t;
 
 }
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 2b3007f02..7e47d0bc8 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -191,7 +191,7 @@ val find_custom_match : ml_branch array -> string
 
 val extraction_language : lang -> unit
 val extraction_inline : bool -> reference list -> unit
-val print_extraction_inline : unit -> Pp.std_ppcmds
+val print_extraction_inline : unit -> Pp.t
 val reset_extraction_inline : unit -> unit
 val extract_constant_inline :
   bool -> reference -> string list -> string -> unit
@@ -206,7 +206,7 @@ val extraction_implicit : reference -> int_or_id list -> unit
 
 val extraction_blacklist : Id.t list -> unit
 val reset_extraction_blacklist : unit -> unit
-val print_extraction_blacklist : unit -> Pp.std_ppcmds
+val print_extraction_blacklist : unit -> Pp.t
 
 
 
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 0a2e84bb8..ca6079c8b 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -57,4 +57,4 @@ val extend_with_ref_list : Environ.env -> Evd.evar_map -> global_reference list
 val extend_with_auto_hints : Environ.env -> Evd.evar_map -> Hints.hint_db_name list ->
   t -> t * Evd.evar_map
 
-val print_cmap: global_reference list CM.t -> Pp.std_ppcmds
+val print_cmap: global_reference list CM.t -> Pp.t
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 7a60da44f..93e03852e 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -1,8 +1,8 @@
 open Misctypes
 
-val warn_cannot_define_graph : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit
+val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit
 
-val warn_cannot_define_principle : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit
+val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit
 
 val do_generate_principle :  
   bool -> 
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 5e425cd18..2e2ced790 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -1,5 +1,4 @@
 open Names
-open Pp
 
 (*
    The mk_?_id function build different name w.r.t. a function
@@ -11,7 +10,7 @@ val mk_complete_id : Id.t -> Id.t
 val mk_equation_id : Id.t -> Id.t
 
 
-val msgnl : std_ppcmds -> unit
+val msgnl : Pp.t -> unit
 
 val fresh_id : Id.t list -> string -> Id.t
 val fresh_name : Id.t list -> string -> Name.t
@@ -24,7 +23,7 @@ val id_of_name : Name.t -> Id.t
 val locate_ind : Libnames.reference -> inductive
 val locate_constant : Libnames.reference -> Constant.t
 val locate_with_msg :
-  Pp.std_ppcmds -> (Libnames.reference -> 'a) ->
+  Pp.t -> (Libnames.reference -> 'a) ->
   Libnames.reference -> 'a
 
 val filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list
@@ -89,8 +88,8 @@ val update_Function : function_info -> unit
 
 
 (** debugging *)
-val pr_info : function_info -> Pp.std_ppcmds
-val pr_table : unit -> Pp.std_ppcmds
+val pr_info : function_info -> Pp.t
+val pr_table : unit -> Pp.t
 
 
 (* val function_debug : bool ref  *)
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index acdf67779..b06f35ddc 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -14,13 +14,13 @@ open Misctypes
 
 val wit_orient : bool Genarg.uniform_genarg_type
 val orient : bool Pcoq.Gram.entry
-val pr_orient : bool -> Pp.std_ppcmds
+val pr_orient : bool -> Pp.t
 
 val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type
 
 val occurrences : (int list or_var) Pcoq.Gram.entry
 val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg_type
-val pr_occurrences : int list or_var -> Pp.std_ppcmds
+val pr_occurrences : int list or_var -> Pp.t
 val occurrences_of : int list -> Locus.occurrences
 
 val wit_natural : int Genarg.uniform_genarg_type
@@ -55,7 +55,7 @@ type place = Id.t gen_place
 
 val wit_hloc : (loc_place, loc_place, place) Genarg.genarg_type
 val hloc : loc_place Pcoq.Gram.entry
-val pr_hloc : loc_place -> Pp.std_ppcmds
+val pr_hloc : loc_place -> Pp.t
 
 val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry
 val wit_by_arg_tac :
@@ -64,8 +64,8 @@ val wit_by_arg_tac :
   Geninterp.Val.t option) Genarg.genarg_type
 
 val pr_by_arg_tac : 
-  (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) ->
-  raw_tactic_expr option -> Pp.std_ppcmds
+  (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.t) ->
+  raw_tactic_expr option -> Pp.t
 
 val test_lpar_id_colon : unit Pcoq.Gram.entry
 
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 327b347ec..140cc3344 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -67,22 +67,22 @@ let declare_notation_tactic_pprule kn pt =
   prnotation_tab := KNmap.add kn pt !prnotation_tab
 
 type 'a raw_extra_genarg_printer =
-    (constr_expr -> std_ppcmds) ->
-    (constr_expr -> std_ppcmds) ->
-    (tolerability -> raw_tactic_expr -> std_ppcmds) ->
-    'a -> std_ppcmds
+    (constr_expr -> Pp.t) ->
+    (constr_expr -> Pp.t) ->
+    (tolerability -> raw_tactic_expr -> Pp.t) ->
+    'a -> Pp.t
 
 type 'a glob_extra_genarg_printer =
-    (glob_constr_and_expr -> std_ppcmds) ->
-    (glob_constr_and_expr -> std_ppcmds) ->
-    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
-    'a -> std_ppcmds
+    (glob_constr_and_expr -> Pp.t) ->
+    (glob_constr_and_expr -> Pp.t) ->
+    (tolerability -> glob_tactic_expr -> Pp.t) ->
+    'a -> Pp.t
 
 type 'a extra_genarg_printer =
-    (EConstr.constr -> std_ppcmds) ->
-    (EConstr.constr -> std_ppcmds) ->
-    (tolerability -> Val.t -> std_ppcmds) ->
-    'a -> std_ppcmds
+    (EConstr.constr -> Pp.t) ->
+    (EConstr.constr -> Pp.t) ->
+    (tolerability -> Val.t -> Pp.t) ->
+    'a -> Pp.t
 
   let keyword x = tag_keyword (str x)
   let primitive x = tag_primitive (str x)
@@ -96,7 +96,7 @@ type 'a extra_genarg_printer =
   | None -> assert false
   | Some Refl -> x
 
-  let rec pr_value lev v : std_ppcmds =
+  let rec pr_value lev v : Pp.t =
     if has_type v Val.typ_list then
       pr_sequence (fun x -> pr_value lev x) (unbox v Val.typ_list)
     else if has_type v Val.typ_opt then
@@ -272,7 +272,7 @@ type 'a extra_genarg_printer =
   | Glbwit (OptArg wit) -> Some (Option.map (in_gen (glbwit wit)) arg)
   | _ -> None
 
-  let rec pr_any_arg : type l. (_ -> l generic_argument -> std_ppcmds) -> _ -> l generic_argument -> std_ppcmds =
+  let rec pr_any_arg : type l. (_ -> l generic_argument -> Pp.t) -> _ -> l generic_argument -> Pp.t =
   fun prtac symb arg -> match symb with
   | Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac (1, Any) arg
   | Extend.Ulist1 s | Extend.Ulist0 s ->
@@ -599,18 +599,18 @@ type 'a extra_genarg_printer =
       "raw", "glob" and "typed" levels *)
 
   type 'a printer = {
-    pr_tactic    : tolerability -> 'tacexpr -> std_ppcmds;
-    pr_constr    : 'trm -> std_ppcmds;
-    pr_lconstr   : 'trm -> std_ppcmds;
-    pr_dconstr   : 'dtrm -> std_ppcmds;
-    pr_pattern   : 'pat -> std_ppcmds;
-    pr_lpattern  : 'pat -> std_ppcmds;
-    pr_constant  : 'cst -> std_ppcmds;
-    pr_reference : 'ref -> std_ppcmds;
-    pr_name      : 'nam -> std_ppcmds;
-    pr_generic   : 'lev generic_argument -> std_ppcmds;
-    pr_extend    : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> std_ppcmds;
-    pr_alias     : int -> KerName.t -> 'a gen_tactic_arg list -> std_ppcmds;
+    pr_tactic    : tolerability -> 'tacexpr -> Pp.t;
+    pr_constr    : 'trm -> Pp.t;
+    pr_lconstr   : 'trm -> Pp.t;
+    pr_dconstr   : 'dtrm -> Pp.t;
+    pr_pattern   : 'pat -> Pp.t;
+    pr_lpattern  : 'pat -> Pp.t;
+    pr_constant  : 'cst -> Pp.t;
+    pr_reference : 'ref -> Pp.t;
+    pr_name      : 'nam -> Pp.t;
+    pr_generic   : 'lev generic_argument -> Pp.t;
+    pr_extend    : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> Pp.t;
+    pr_alias     : int -> KerName.t -> 'a gen_tactic_arg list -> Pp.t;
   }
 
   constraint 'a = <
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 1127c9831..0bf9bc7f6 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -9,7 +9,6 @@
 (** This module implements pretty-printers for tactic_expr syntactic
     objects and their subcomponents. *)
 
-open Pp
 open Genarg
 open Geninterp
 open Names
@@ -24,22 +23,22 @@ type 'a grammar_tactic_prod_item_expr =
 | TacNonTerm of ('a * Names.Id.t option) Loc.located
 
 type 'a raw_extra_genarg_printer =
-    (constr_expr -> std_ppcmds) ->
-    (constr_expr -> std_ppcmds) ->
-    (tolerability -> raw_tactic_expr -> std_ppcmds) ->
-    'a -> std_ppcmds
+    (constr_expr -> Pp.t) ->
+    (constr_expr -> Pp.t) ->
+    (tolerability -> raw_tactic_expr -> Pp.t) ->
+    'a -> Pp.t
 
 type 'a glob_extra_genarg_printer =
-    (glob_constr_and_expr -> std_ppcmds) ->
-    (glob_constr_and_expr -> std_ppcmds) ->
-    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
-    'a -> std_ppcmds
+    (glob_constr_and_expr -> Pp.t) ->
+    (glob_constr_and_expr -> Pp.t) ->
+    (tolerability -> glob_tactic_expr -> Pp.t) ->
+    'a -> Pp.t
 
 type 'a extra_genarg_printer =
-    (EConstr.t -> std_ppcmds) ->
-    (EConstr.t -> std_ppcmds) ->
-    (tolerability -> Val.t -> std_ppcmds) ->
-    'a -> std_ppcmds
+    (EConstr.t -> Pp.t) ->
+    (EConstr.t -> Pp.t) ->
+    (tolerability -> Val.t -> Pp.t) ->
+    'a -> Pp.t
 
 val declare_extra_genarg_pprule :
   ('a, 'b, 'c) genarg_type ->
@@ -57,61 +56,61 @@ type pp_tactic = {
 val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
 
 val pr_with_occurrences :
-  ('a -> std_ppcmds) -> 'a Locus.with_occurrences -> std_ppcmds
+  ('a -> Pp.t) -> 'a Locus.with_occurrences -> Pp.t
 val pr_red_expr :
-  ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) ->
-  ('a,'b,'c) Genredexpr.red_expr_gen -> std_ppcmds
+  ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) ->
+  ('a,'b,'c) Genredexpr.red_expr_gen -> Pp.t
 val pr_may_eval :
-  ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
-  ('c -> std_ppcmds) -> ('a,'b,'c) Genredexpr.may_eval -> std_ppcmds
+  ('a -> Pp.t) -> ('a -> Pp.t) -> ('b -> Pp.t) ->
+  ('c -> Pp.t) -> ('a,'b,'c) Genredexpr.may_eval -> Pp.t
 
-val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
-val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds
+val pr_and_short_name : ('a -> Pp.t) -> 'a and_short_name -> Pp.t
+val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t
 
 val pr_in_clause :
-  ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
+  ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t
 
 val pr_clauses :  bool option ->
-  ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
+  ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t
 
-val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds
+val pr_raw_generic : env -> rlevel generic_argument -> Pp.t
 
-val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds
+val pr_glb_generic : env -> glevel generic_argument -> Pp.t
 
 val pr_raw_extend: env -> int ->
-  ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds
+  ml_tactic_entry -> raw_tactic_arg list -> Pp.t
 
 val pr_glob_extend: env -> int ->
-  ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds
+  ml_tactic_entry -> glob_tactic_arg list -> Pp.t
 
 val pr_extend :
-  (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds
+  (Val.t -> Pp.t) -> int -> ml_tactic_entry -> Val.t list -> Pp.t
 
-val pr_alias_key : Names.KerName.t -> std_ppcmds
+val pr_alias_key : Names.KerName.t -> Pp.t
 
-val pr_alias : (Val.t -> std_ppcmds) ->
-  int -> Names.KerName.t -> Val.t list -> std_ppcmds
+val pr_alias : (Val.t -> Pp.t) ->
+  int -> Names.KerName.t -> Val.t list -> Pp.t
 
-val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
+val pr_ltac_constant : Nametab.ltac_constant -> Pp.t
 
-val pr_raw_tactic : raw_tactic_expr -> std_ppcmds
+val pr_raw_tactic : raw_tactic_expr -> Pp.t
 
-val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> std_ppcmds
+val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> Pp.t
 
-val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
+val pr_glob_tactic : env -> glob_tactic_expr -> Pp.t
 
-val pr_atomic_tactic : env -> Evd.evar_map -> atomic_tactic_expr -> std_ppcmds
+val pr_atomic_tactic : env -> Evd.evar_map -> atomic_tactic_expr -> Pp.t
 
-val pr_hintbases : string list option -> std_ppcmds
+val pr_hintbases : string list option -> Pp.t
 
-val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds
+val pr_auto_using : ('constr -> Pp.t) -> 'constr list -> Pp.t
 
-val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
+val pr_match_pattern : ('a -> Pp.t) -> 'a match_pattern -> Pp.t
 
-val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
-  ('b, 'a) match_rule -> std_ppcmds
+val pr_match_rule : bool -> ('a -> Pp.t) -> ('b -> Pp.t) ->
+  ('b, 'a) match_rule -> Pp.t
 
-val pr_value : tolerability -> Val.t -> std_ppcmds
+val pr_value : tolerability -> Val.t -> Pp.t
 
 
 val ltop : tolerability
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index bbd7834d5..75b665aad 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1461,7 +1461,7 @@ let solve_constraints env (evars,cstrs) =
 let nf_zeta =
   Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
 
-exception RewriteFailure of Pp.std_ppcmds
+exception RewriteFailure of Pp.t
 
 type result = (evar_map * constr option * types) option option
 
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 35205ac58..23767c12f 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -61,8 +61,8 @@ val strategy_of_ast : (glob_constr_and_expr, raw_red_expr) strategy_ast -> strat
 val map_strategy : ('a -> 'b) -> ('c -> 'd) ->
   ('a, 'c) strategy_ast -> ('b, 'd) strategy_ast
 
-val pr_strategy : ('a -> Pp.std_ppcmds) -> ('b -> Pp.std_ppcmds) ->
-  ('a, 'b) strategy_ast -> Pp.std_ppcmds
+val pr_strategy : ('a -> Pp.t) -> ('b -> Pp.t) ->
+  ('a, 'b) strategy_ast -> Pp.t
 
 (** Entry point for user-level "rewrite_strat" *)
 val cl_rewrite_clause_strat : strategy -> Id.t option -> unit Proofview.tactic
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index b262473a9..e3a4d5c79 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Names
 open Tacexpr
 open Genarg
@@ -55,7 +54,7 @@ val intern_hyp : glob_sign -> Id.t Loc.located -> Id.t Loc.located
 val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument
 
 (** printing *)
-val print_ltac : Libnames.qualid -> std_ppcmds
+val print_ltac : Libnames.qualid -> Pp.t
 
 (** Reduction expressions *)
 
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index ef6362270..2475e41f9 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -58,16 +58,16 @@ val db_hyp_pattern_failure :
 val db_matching_failure : debug_info -> unit Proofview.NonLogical.t
 
 (** Prints an evaluation failure message for a rule *)
-val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit Proofview.NonLogical.t
+val db_eval_failure : debug_info -> Pp.t -> unit Proofview.NonLogical.t
 
 (** An exception handler *)
-val explain_logic_error: exn -> Pp.std_ppcmds
+val explain_logic_error: exn -> Pp.t
 
 (** For use in the Ltac debugger: some exception that are usually
    consider anomalies are acceptable because they are caught later in
    the process that is being debugged.  One should not require
    from users that they report these anomalies. *)
-val explain_logic_error_no_anomaly : exn -> Pp.std_ppcmds
+val explain_logic_error_no_anomaly : exn -> Pp.t
 
 (** Prints a logic failure message for a rule *)
 val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t
@@ -77,4 +77,4 @@ val db_breakpoint : debug_info ->
   Id.t Loc.located message_token list -> unit Proofview.NonLogical.t
 
 val extract_ltac_trace :
-  ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.std_ppcmds option Loc.located
+  ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t option Loc.located
diff --git a/plugins/ltac/tactic_option.mli b/plugins/ltac/tactic_option.mli
index dd91944d4..95cd243ec 100644
--- a/plugins/ltac/tactic_option.mli
+++ b/plugins/ltac/tactic_option.mli
@@ -12,4 +12,4 @@ open Vernacexpr
 val declare_tactic_option : ?default:Tacexpr.glob_tactic_expr -> string -> 
   (* put *) (locality_flag -> glob_tactic_expr -> unit) *
   (* get *) (unit -> locality_flag * unit Proofview.tactic) *
-  (* print *) (unit -> Pp.std_ppcmds)
+  (* print *) (unit -> Pp.t)
diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli
index e0c09f394..86231cf19 100644
--- a/plugins/rtauto/proof_search.mli
+++ b/plugins/rtauto/proof_search.mli
@@ -38,9 +38,9 @@ val branching: state -> state list
 
 val success: state -> bool
 
-val pp: state -> Pp.std_ppcmds
+val pp: state -> Pp.t
 
-val pr_form : form -> Pp.std_ppcmds
+val pr_form : form -> Pp.t
 
 val reset_info : unit -> unit
 
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 4b045e989..2eadd5f26 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -41,7 +41,7 @@ val nohint : 'a ssrhint
 
 (******************************** misc ************************************)
 
-val errorstrm : Pp.std_ppcmds -> 'a
+val errorstrm : Pp.t -> 'a
 val anomaly : string -> 'a
 
 val array_app_tl : 'a array -> 'a list -> 'a list
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index bf6f44f11..88beeaa71 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -16,5 +16,5 @@ val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
 val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
 val pr_ssrtclarg : 'a -> 'b -> (int * Ppextend.parenRelation -> 'c -> 'd) -> 'c -> 'd
 
-val add_genarg : string -> ('a -> Pp.std_ppcmds) -> 'a Genarg.uniform_genarg_type
+val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type
 
diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli
index 5c68872b7..f23106826 100644
--- a/plugins/ssr/ssrprinters.mli
+++ b/plugins/ssr/ssrprinters.mli
@@ -11,16 +11,16 @@
 open Ssrast
 
 val pp_term :
-  Goal.goal Evd.sigma -> EConstr.constr -> Pp.std_ppcmds
+  Goal.goal Evd.sigma -> EConstr.constr -> Pp.t
 
-val pr_spc : unit -> Pp.std_ppcmds
-val pr_bar : unit -> Pp.std_ppcmds
+val pr_spc : unit -> Pp.t
+val pr_bar : unit -> Pp.t
 val pr_list : 
-  (unit -> Pp.std_ppcmds) -> ('a -> Pp.std_ppcmds) -> 'a list -> Pp.std_ppcmds
+  (unit -> Pp.t) -> ('a -> Pp.t) -> 'a list -> Pp.t
 
 val pp_concat :
-  Pp.std_ppcmds ->
-  ?sep:Pp.std_ppcmds -> Pp.std_ppcmds list -> Pp.std_ppcmds
+  Pp.t ->
+  ?sep:Pp.t -> Pp.t list -> Pp.t
 
 val xInParens : ssrtermkind
 val xWithAt : ssrtermkind
@@ -29,17 +29,17 @@ val xCpattern : ssrtermkind
 
 val pr_term :
   ssrtermkind * (Glob_term.glob_constr * Constrexpr.constr_expr option) ->
-  Pp.std_ppcmds
+  Pp.t
 
-val pr_hyp : ssrhyp -> Pp.std_ppcmds
+val pr_hyp : ssrhyp -> Pp.t
 
-val prl_constr_expr : Constrexpr.constr_expr -> Pp.std_ppcmds
-val prl_glob_constr : Glob_term.glob_constr -> Pp.std_ppcmds
+val prl_constr_expr : Constrexpr.constr_expr -> Pp.t
+val prl_glob_constr : Glob_term.glob_constr -> Pp.t
 
 val pr_guarded :
-  (string -> int -> bool) -> ('a -> Pp.std_ppcmds) -> 'a -> Pp.std_ppcmds
+  (string -> int -> bool) -> ('a -> Pp.t) -> 'a -> Pp.t
 
-val pr_occ : ssrocc -> Pp.std_ppcmds
+val pr_occ : ssrocc -> Pp.t
 
-val ppdebug : Pp.std_ppcmds Lazy.t -> unit
+val ppdebug : Pp.t Lazy.t -> unit
 
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 65ea76d16..8e2a1a717 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -15,7 +15,7 @@ open Term
 (** The type of context patterns, the patterns of the [set] tactic and 
     [:] tactical. These are patterns that identify a precise subterm. *)
 type cpattern
-val pr_cpattern : cpattern -> Pp.std_ppcmds
+val pr_cpattern : cpattern -> Pp.t
 
 (** CS cpattern: (f _), (X in t), (t in X in t), (t as X in t) *)
 val cpattern         : cpattern Pcoq.Gram.entry
@@ -29,7 +29,7 @@ val wit_lcpattern     : cpattern uniform_genarg_type
     These patterns also include patterns that identify all the subterms
     of a context (i.e. "in" prefix) *)
 type rpattern
-val pr_rpattern : rpattern -> Pp.std_ppcmds
+val pr_rpattern : rpattern -> Pp.t
 
 (** OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t *)
 val rpattern         : rpattern Pcoq.Gram.entry
@@ -50,7 +50,7 @@ type ('ident, 'term) ssrpattern =
   | E_As_X_In_T of 'term * 'ident * 'term
 
 type pattern = evar_map * (constr, constr) ssrpattern
-val pp_pattern : pattern -> Pp.std_ppcmds
+val pp_pattern : pattern -> Pp.t
 
 (** Extracts the redex and applies to it the substitution part of the pattern.
   @raise Anomaly if called on [In_T] or [In_X_In_T] *)
@@ -115,7 +115,7 @@ val fill_occ_pattern :
    the T pattern above, and calls a continuation on its occurrences. *)
 
 type ssrdir = L2R | R2L
-val pr_dir_side : ssrdir -> Pp.std_ppcmds
+val pr_dir_side : ssrdir -> Pp.t
 
 (** a pattern for a term with wildcards *)
 type tpattern
@@ -225,7 +225,7 @@ val loc_of_cpattern : cpattern -> Loc.t option
 val id_of_pattern : pattern -> Names.Id.t option
 val is_wildcard : cpattern -> bool
 val cpattern_of_id : Names.Id.t -> cpattern
-val pr_constr_pat : constr -> Pp.std_ppcmds
+val pr_constr_pat : constr -> Pp.t
 val pf_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma
 val pf_unsafe_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma