deprecate Pp.std_ppcmds type alias

11 files changed, 202 insertions, 209 deletions

diff --git a/printing/genprint.ml b/printing/genprint.ml
index bb9736d73..543b05024 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -9,7 +9,7 @@
 open Pp
 open Genarg
 
-type 'a printer = 'a -> std_ppcmds
+type 'a printer = 'a -> Pp.t
 
 type ('raw, 'glb, 'top) genprinter = {
   raw : 'raw printer;
diff --git a/printing/genprint.mli b/printing/genprint.mli
index 24779a359..130a89c92 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -8,18 +8,17 @@
 
 (** Entry point for generic printers *)
 
-open Pp
 open Genarg
 
-type 'a printer = 'a -> std_ppcmds
+type 'a printer = 'a -> Pp.t
 
-val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw -> std_ppcmds
+val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw -> Pp.t
 (** Printer for raw level generic arguments. *)
 
-val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb -> std_ppcmds
+val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb -> Pp.t
 (** Printer for glob level generic arguments. *)
 
-val top_print : ('raw, 'glb, 'top) genarg_type -> 'top -> std_ppcmds
+val top_print : ('raw, 'glb, 'top) genarg_type -> 'top -> Pp.t
 (** Printer for top level generic arguments. *)
 
 val generic_raw_print : rlevel generic_argument printer
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index cf513321f..ee03bc900 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -731,10 +731,10 @@ let tag_var = tag Tag.variable
       (sep() ++ if prec_less prec inherited then strm else surround strm)
 
   type term_pr = {
-    pr_constr_expr   : constr_expr -> std_ppcmds;
-    pr_lconstr_expr  : constr_expr -> std_ppcmds;
-    pr_constr_pattern_expr  : constr_pattern_expr -> std_ppcmds;
-    pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
+    pr_constr_expr   : constr_expr -> Pp.t;
+    pr_lconstr_expr  : constr_expr -> Pp.t;
+    pr_constr_pattern_expr  : constr_pattern_expr -> Pp.t;
+    pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
   }
 
   type precedence =  Ppextend.precedence * Ppextend.parenRelation
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index fd232759e..833503485 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -9,10 +9,8 @@
 (** This module implements pretty-printers for constr_expr syntactic
     objects and their subcomponents. *)
 
-(** The default pretty-printers produce {!Pp.std_ppcmds} that are
-    interpreted as raw strings. *)
+(** The default pretty-printers produce pretty-printing commands ({!Pp.t}). *)
 open Loc
-open Pp
 open Libnames
 open Constrexpr
 open Names
@@ -28,45 +26,45 @@ val split_fix :
 
 val prec_less : int -> int * Ppextend.parenRelation -> bool
 
-val pr_tight_coma : unit -> std_ppcmds
+val pr_tight_coma : unit -> Pp.t
 
-val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
+val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t
 
-val pr_lident : Id.t located -> std_ppcmds
-val pr_lname : Name.t located -> std_ppcmds
+val pr_lident : Id.t located -> Pp.t
+val pr_lname : Name.t located -> Pp.t
 
-val pr_with_comments : ?loc:Loc.t -> std_ppcmds -> std_ppcmds
-val pr_com_at : int -> std_ppcmds
+val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t
+val pr_com_at : int -> Pp.t
 val pr_sep_com :
-  (unit -> std_ppcmds) ->
-  (constr_expr -> std_ppcmds) ->
-  constr_expr -> std_ppcmds
+  (unit -> Pp.t) ->
+  (constr_expr -> Pp.t) ->
+  constr_expr -> Pp.t
 
-val pr_id : Id.t -> std_ppcmds
-val pr_name : Name.t -> std_ppcmds
-val pr_qualid : qualid -> std_ppcmds
-val pr_patvar : patvar -> std_ppcmds
+val pr_id : Id.t -> Pp.t
+val pr_name : Name.t -> Pp.t
+val pr_qualid : qualid -> Pp.t
+val pr_patvar : patvar -> Pp.t
 
-val pr_glob_level : glob_level -> std_ppcmds
-val pr_glob_sort : glob_sort -> std_ppcmds
-val pr_guard_annot : (constr_expr -> std_ppcmds) ->
+val pr_glob_level : glob_level -> Pp.t
+val pr_glob_sort : glob_sort -> Pp.t
+val pr_guard_annot : (constr_expr -> Pp.t) ->
   local_binder_expr list ->
   ('a * Names.Id.t) option * recursion_order_expr ->
-  std_ppcmds
+  Pp.t
 
-val pr_record_body : (reference * constr_expr) list -> std_ppcmds
-val pr_binders : local_binder_expr list -> std_ppcmds
-val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds
-val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
-val pr_constr_expr : constr_expr -> std_ppcmds
-val pr_lconstr_expr : constr_expr -> std_ppcmds
-val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds
+val pr_record_body : (reference * constr_expr) list -> Pp.t
+val pr_binders : local_binder_expr list -> Pp.t
+val pr_constr_pattern_expr : constr_pattern_expr -> Pp.t
+val pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
+val pr_constr_expr : constr_expr -> Pp.t
+val pr_lconstr_expr : constr_expr -> Pp.t
+val pr_cases_pattern_expr : cases_pattern_expr -> Pp.t
 
 type term_pr = {
-  pr_constr_expr   : constr_expr -> std_ppcmds;
-  pr_lconstr_expr  : constr_expr -> std_ppcmds;
-  pr_constr_pattern_expr  : constr_pattern_expr -> std_ppcmds;
-  pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
+  pr_constr_expr   : constr_expr -> Pp.t;
+  pr_lconstr_expr  : constr_expr -> Pp.t;
+  pr_constr_pattern_expr  : constr_pattern_expr -> Pp.t;
+  pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
 }
 
 val set_term_pr : term_pr -> unit
@@ -91,5 +89,5 @@ type precedence
 val lsimpleconstr : precedence
 val ltop : precedence
 val modular_constr_pr :
-  ((unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds) ->
-  (unit->std_ppcmds) -> precedence  -> constr_expr -> std_ppcmds
+  ((unit->Pp.t) -> precedence -> constr_expr -> Pp.t) ->
+  (unit->Pp.t) -> precedence  -> constr_expr -> Pp.t
diff --git a/printing/pputils.mli b/printing/pputils.mli
index 0dee11e0b..1f4fa1390 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -6,26 +6,25 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Genarg
 open Misctypes
 open Locus
 open Genredexpr
 
-val pr_located : ('a -> std_ppcmds) -> 'a Loc.located -> std_ppcmds
+val pr_located : ('a -> Pp.t) -> 'a Loc.located -> Pp.t
 (** Prints an object surrounded by its commented location *)
 
-val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
-val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds
+val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t
+val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t
 val pr_with_occurrences :
-  ('a -> std_ppcmds) -> (string -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds
+  ('a -> Pp.t) -> (string -> Pp.t) -> 'a with_occurrences -> Pp.t
 
-val pr_short_red_flag : ('a -> std_ppcmds) -> 'a glob_red_flag -> std_ppcmds
-val pr_red_flag : ('a -> std_ppcmds) -> 'a glob_red_flag -> std_ppcmds
+val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
+val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
 val pr_red_expr :
-  ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) ->
-  (string -> std_ppcmds) ->
-  ('a,'b,'c) red_expr_gen -> std_ppcmds
+  ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) ->
+  (string -> Pp.t) ->
+  ('a,'b,'c) red_expr_gen -> Pp.t
 
-val pr_raw_generic : Environ.env -> rlevel generic_argument -> std_ppcmds
-val pr_glb_generic : Environ.env -> glevel generic_argument -> std_ppcmds
+val pr_raw_generic : Environ.env -> rlevel generic_argument -> Pp.t
+val pr_glb_generic : Environ.env -> glevel generic_argument -> Pp.t
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
index ed5585b30..b88eed484 100644
--- a/printing/ppvernac.mli
+++ b/printing/ppvernac.mli
@@ -10,10 +10,10 @@
     objects and their subcomponents. *)
 
 (** Prints a fixpoint body *)
-val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.std_ppcmds
+val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t
 
 (** Prints a vernac expression *)
-val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.std_ppcmds
+val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.t
 
 (** Prints a vernac expression and closes it with a dot. *)
-val pr_vernac : Vernacexpr.vernac_expr -> Pp.std_ppcmds
+val pr_vernac : Vernacexpr.vernac_expr -> Pp.t
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 827c0e458..e0ebe99db 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -33,17 +33,17 @@ open Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
 type object_pr = {
-  print_inductive           : mutual_inductive -> std_ppcmds;
-  print_constant_with_infos : constant -> std_ppcmds;
-  print_section_variable    : variable -> std_ppcmds;
-  print_syntactic_def       : kernel_name -> std_ppcmds;
-  print_module              : bool -> Names.module_path -> std_ppcmds;
-  print_modtype             : module_path -> std_ppcmds;
-  print_named_decl          : Context.Named.Declaration.t -> std_ppcmds;
-  print_library_entry       : bool -> (object_name * Lib.node) -> std_ppcmds option;
-  print_context             : bool -> int option -> Lib.library_segment -> std_ppcmds;
-  print_typed_value_in_env  : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.std_ppcmds;
-  print_eval                : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> std_ppcmds;
+  print_inductive           : mutual_inductive -> Pp.t;
+  print_constant_with_infos : constant -> Pp.t;
+  print_section_variable    : variable -> Pp.t;
+  print_syntactic_def       : kernel_name -> Pp.t;
+  print_module              : bool -> Names.module_path -> Pp.t;
+  print_modtype             : module_path -> Pp.t;
+  print_named_decl          : Context.Named.Declaration.t -> Pp.t;
+  print_library_entry       : bool -> (object_name * Lib.node) -> Pp.t option;
+  print_context             : bool -> int option -> Lib.library_segment -> Pp.t;
+  print_typed_value_in_env  : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t;
+  print_eval                : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t;
 }
 
 let gallina_print_module  = print_module
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 4add21fa7..f4277b6c5 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Names
 open Environ
 open Reductionops
@@ -19,57 +18,57 @@ open Misctypes
 val assumptions_for_print : Name.t list -> Termops.names_context
 
 val print_closed_sections : bool ref
-val print_context : bool -> int option -> Lib.library_segment -> std_ppcmds
-val print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option
-val print_full_context : unit -> std_ppcmds
-val print_full_context_typ : unit -> std_ppcmds
-val print_full_pure_context : unit -> std_ppcmds
-val print_sec_context : reference -> std_ppcmds
-val print_sec_context_typ : reference -> std_ppcmds
-val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> std_ppcmds
-val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> std_ppcmds
+val print_context : bool -> int option -> Lib.library_segment -> Pp.t
+val print_library_entry : bool -> (object_name * Lib.node) -> Pp.t option
+val print_full_context : unit -> Pp.t
+val print_full_context_typ : unit -> Pp.t
+val print_full_pure_context : unit -> Pp.t
+val print_sec_context : reference -> Pp.t
+val print_sec_context_typ : reference -> Pp.t
+val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t
+val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t
 val print_eval :
   reduction_function -> env -> Evd.evar_map ->
-    Constrexpr.constr_expr -> EConstr.unsafe_judgment -> std_ppcmds
+    Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
 
-val print_name : reference or_by_notation -> std_ppcmds
-val print_opaque_name : reference -> std_ppcmds
-val print_about : reference or_by_notation -> std_ppcmds
-val print_impargs : reference or_by_notation -> std_ppcmds
+val print_name : reference or_by_notation -> Pp.t
+val print_opaque_name : reference -> Pp.t
+val print_about : reference or_by_notation -> Pp.t
+val print_impargs : reference or_by_notation -> Pp.t
 
 (** Pretty-printing functions for classes and coercions *)
-val print_graph : unit -> std_ppcmds
-val print_classes : unit -> std_ppcmds
-val print_coercions : unit -> std_ppcmds
-val print_path_between : Classops.cl_typ -> Classops.cl_typ -> std_ppcmds
-val print_canonical_projections : unit -> std_ppcmds
+val print_graph : unit -> Pp.t
+val print_classes : unit -> Pp.t
+val print_coercions : unit -> Pp.t
+val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t
+val print_canonical_projections : unit -> Pp.t
 
 (** Pretty-printing functions for type classes and instances *)
-val print_typeclasses : unit -> std_ppcmds
-val print_instances : global_reference -> std_ppcmds
-val print_all_instances : unit -> std_ppcmds
+val print_typeclasses : unit -> Pp.t
+val print_instances : global_reference -> Pp.t
+val print_all_instances : unit -> Pp.t
 
-val inspect : int -> std_ppcmds
+val inspect : int -> Pp.t
 
 (** Locate *)
 
-val print_located_qualid : reference -> std_ppcmds
-val print_located_term : reference -> std_ppcmds
-val print_located_tactic : reference -> std_ppcmds
-val print_located_module : reference -> std_ppcmds
+val print_located_qualid : reference -> Pp.t
+val print_located_term : reference -> Pp.t
+val print_located_tactic : reference -> Pp.t
+val print_located_module : reference -> Pp.t
 
 type object_pr = {
-  print_inductive           : mutual_inductive -> std_ppcmds;
-  print_constant_with_infos : constant -> std_ppcmds;
-  print_section_variable    : variable -> std_ppcmds;
-  print_syntactic_def       : kernel_name -> std_ppcmds;
-  print_module              : bool -> Names.module_path -> std_ppcmds;
-  print_modtype             : module_path -> std_ppcmds;
-  print_named_decl          : Context.Named.Declaration.t -> std_ppcmds;
-  print_library_entry       : bool -> (object_name * Lib.node) -> std_ppcmds option;
-  print_context             : bool -> int option -> Lib.library_segment -> std_ppcmds;
-  print_typed_value_in_env  : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.std_ppcmds;
-  print_eval                : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> std_ppcmds
+  print_inductive           : mutual_inductive -> Pp.t;
+  print_constant_with_infos : constant -> Pp.t;
+  print_section_variable    : variable -> Pp.t;
+  print_syntactic_def       : kernel_name -> Pp.t;
+  print_module              : bool -> Names.module_path -> Pp.t;
+  print_modtype             : module_path -> Pp.t;
+  print_named_decl          : Context.Named.Declaration.t -> Pp.t;
+  print_library_entry       : bool -> (object_name * Lib.node) -> Pp.t option;
+  print_context             : bool -> int option -> Lib.library_segment -> Pp.t;
+  print_typed_value_in_env  : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t;
+  print_eval                : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
 }
 
 val set_object_pr : object_pr -> unit
diff --git a/printing/printer.ml b/printing/printer.ml
index 351678802..f731a39a4 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -758,9 +758,9 @@ let default_pr_subgoals ?(pr_first=true)
 
 
 type printer_pr = {
- pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> std_ppcmds;
- pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
- pr_goal                : goal sigma -> std_ppcmds;
+ pr_subgoals            : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t;
+ pr_subgoal             : int -> evar_map -> goal list -> Pp.t;
+ pr_goal                : goal sigma -> Pp.t;
 }
 
 let default_printer_pr = {
diff --git a/printing/printer.mli b/printing/printer.mli
index f8685b089..2c9a4d70e 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Names
 open Globnames
 open Term
@@ -25,96 +24,96 @@ val enable_goal_names_printing     : bool ref
 
 (** Terms *)
 
-val pr_lconstr_env         : env -> evar_map -> constr -> std_ppcmds
-val pr_lconstr             : constr -> std_ppcmds
-val pr_lconstr_goal_style_env : env -> evar_map -> constr -> std_ppcmds
+val pr_lconstr_env         : env -> evar_map -> constr -> Pp.t
+val pr_lconstr             : constr -> Pp.t
+val pr_lconstr_goal_style_env : env -> evar_map -> constr -> Pp.t
 
-val pr_constr_env          : env -> evar_map -> constr -> std_ppcmds
-val pr_constr              : constr -> std_ppcmds
-val pr_constr_goal_style_env : env -> evar_map -> constr -> std_ppcmds
+val pr_constr_env          : env -> evar_map -> constr -> Pp.t
+val pr_constr              : constr -> Pp.t
+val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t
 
 (** Same, but resilient to [Nametab] errors. Prints fully-qualified
     names when [shortest_qualid_of_global] has failed. Prints "??"
     in case of remaining issues (such as reference not in env). *)
 
-val safe_pr_lconstr_env         : env -> evar_map -> constr -> std_ppcmds
-val safe_pr_lconstr             : constr -> std_ppcmds
+val safe_pr_lconstr_env         : env -> evar_map -> constr -> Pp.t
+val safe_pr_lconstr             : constr -> Pp.t
 
-val safe_pr_constr_env          : env -> evar_map -> constr -> std_ppcmds
-val safe_pr_constr              : constr -> std_ppcmds
+val safe_pr_constr_env          : env -> evar_map -> constr -> Pp.t
+val safe_pr_constr              : constr -> Pp.t
 
-val pr_econstr_env     : env -> evar_map -> EConstr.t -> std_ppcmds
-val pr_econstr         : EConstr.t -> std_ppcmds
-val pr_leconstr_env     : env -> evar_map -> EConstr.t -> std_ppcmds
-val pr_leconstr         : EConstr.t -> std_ppcmds
+val pr_econstr_env     : env -> evar_map -> EConstr.t -> Pp.t
+val pr_econstr         : EConstr.t -> Pp.t
+val pr_leconstr_env     : env -> evar_map -> EConstr.t -> Pp.t
+val pr_leconstr         : EConstr.t -> Pp.t
 
-val pr_etype_env           : env -> evar_map -> EConstr.types -> std_ppcmds
-val pr_letype_env           : env -> evar_map -> EConstr.types -> std_ppcmds
+val pr_etype_env           : env -> evar_map -> EConstr.types -> Pp.t
+val pr_letype_env           : env -> evar_map -> EConstr.types -> Pp.t
 
-val pr_open_constr_env     : env -> evar_map -> open_constr -> std_ppcmds
-val pr_open_constr         : open_constr -> std_ppcmds
+val pr_open_constr_env     : env -> evar_map -> open_constr -> Pp.t
+val pr_open_constr         : open_constr -> Pp.t
 
-val pr_open_lconstr_env    : env -> evar_map -> open_constr -> std_ppcmds
-val pr_open_lconstr        : open_constr -> std_ppcmds
+val pr_open_lconstr_env    : env -> evar_map -> open_constr -> Pp.t
+val pr_open_lconstr        : open_constr -> Pp.t
 
-val pr_constr_under_binders_env  : env -> evar_map -> constr_under_binders -> std_ppcmds
-val pr_constr_under_binders      : constr_under_binders -> std_ppcmds
+val pr_constr_under_binders_env  : env -> evar_map -> constr_under_binders -> Pp.t
+val pr_constr_under_binders      : constr_under_binders -> Pp.t
 
-val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> std_ppcmds
-val pr_lconstr_under_binders     : constr_under_binders -> std_ppcmds
+val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t
+val pr_lconstr_under_binders     : constr_under_binders -> Pp.t
 
-val pr_goal_concl_style_env : env -> evar_map -> EConstr.types -> std_ppcmds
-val pr_ltype_env           : env -> evar_map -> types -> std_ppcmds
-val pr_ltype               : types -> std_ppcmds
+val pr_goal_concl_style_env : env -> evar_map -> EConstr.types -> Pp.t
+val pr_ltype_env           : env -> evar_map -> types -> Pp.t
+val pr_ltype               : types -> Pp.t
 
-val pr_type_env            : env -> evar_map -> types -> std_ppcmds
-val pr_type                : types -> std_ppcmds
+val pr_type_env            : env -> evar_map -> types -> Pp.t
+val pr_type                : types -> Pp.t
 
-val pr_closed_glob_env     : env -> evar_map -> closed_glob_constr -> std_ppcmds
-val pr_closed_glob         : closed_glob_constr -> std_ppcmds
+val pr_closed_glob_env     : env -> evar_map -> closed_glob_constr -> Pp.t
+val pr_closed_glob         : closed_glob_constr -> Pp.t
 
-val pr_ljudge_env          : env -> evar_map -> EConstr.unsafe_judgment -> std_ppcmds * std_ppcmds
-val pr_ljudge              : EConstr.unsafe_judgment -> std_ppcmds * std_ppcmds
+val pr_ljudge_env          : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t
+val pr_ljudge              : EConstr.unsafe_judgment -> Pp.t * Pp.t
 
-val pr_lglob_constr_env      : env -> glob_constr -> std_ppcmds
-val pr_lglob_constr          : glob_constr -> std_ppcmds
+val pr_lglob_constr_env      : env -> glob_constr -> Pp.t
+val pr_lglob_constr          : glob_constr -> Pp.t
 
-val pr_glob_constr_env       : env -> glob_constr -> std_ppcmds
-val pr_glob_constr           : glob_constr -> std_ppcmds
+val pr_glob_constr_env       : env -> glob_constr -> Pp.t
+val pr_glob_constr           : glob_constr -> Pp.t
 
-val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> std_ppcmds
-val pr_lconstr_pattern     : constr_pattern -> std_ppcmds
+val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t
+val pr_lconstr_pattern     : constr_pattern -> Pp.t
 
-val pr_constr_pattern_env  : env -> evar_map -> constr_pattern -> std_ppcmds
-val pr_constr_pattern      : constr_pattern -> std_ppcmds
+val pr_constr_pattern_env  : env -> evar_map -> constr_pattern -> Pp.t
+val pr_constr_pattern      : constr_pattern -> Pp.t
 
-val pr_cases_pattern       : cases_pattern -> std_ppcmds
+val pr_cases_pattern       : cases_pattern -> Pp.t
 
-val pr_sort                : evar_map -> sorts -> std_ppcmds
+val pr_sort                : evar_map -> sorts -> Pp.t
 
 (** Universe constraints *)
 
-val pr_polymorphic         : bool -> std_ppcmds
-val pr_cumulative          : bool -> bool -> std_ppcmds
-val pr_universe_instance   : evar_map -> Univ.universe_context -> std_ppcmds
-val pr_universe_ctx        : evar_map -> Univ.universe_context -> std_ppcmds
-val pr_cumulativity_info   : evar_map -> Univ.cumulativity_info -> std_ppcmds
+val pr_polymorphic         : bool -> Pp.t
+val pr_cumulative          : bool -> bool -> Pp.t
+val pr_universe_instance   : evar_map -> Univ.universe_context -> Pp.t
+val pr_universe_ctx        : evar_map -> Univ.universe_context -> Pp.t
+val pr_cumulativity_info   : evar_map -> Univ.cumulativity_info -> Pp.t
 
 (** Printing global references using names as short as possible *)
 
-val pr_global_env          : Id.Set.t -> global_reference -> std_ppcmds
-val pr_global              : global_reference -> std_ppcmds
+val pr_global_env          : Id.Set.t -> global_reference -> Pp.t
+val pr_global              : global_reference -> Pp.t
 
-val pr_constant            : env -> constant -> std_ppcmds
-val pr_existential_key     : evar_map -> existential_key -> std_ppcmds
-val pr_existential         : env -> evar_map -> existential -> std_ppcmds
-val pr_constructor         : env -> constructor -> std_ppcmds
-val pr_inductive           : env -> inductive -> std_ppcmds
-val pr_evaluable_reference : evaluable_global_reference -> std_ppcmds
+val pr_constant            : env -> constant -> Pp.t
+val pr_existential_key     : evar_map -> existential_key -> Pp.t
+val pr_existential         : env -> evar_map -> existential -> Pp.t
+val pr_constructor         : env -> constructor -> Pp.t
+val pr_inductive           : env -> inductive -> Pp.t
+val pr_evaluable_reference : evaluable_global_reference -> Pp.t
 
-val pr_pconstant           : env -> pconstant -> std_ppcmds
-val pr_pinductive          : env -> pinductive -> std_ppcmds
-val pr_pconstructor        : env -> pconstructor -> std_ppcmds
+val pr_pconstant           : env -> pconstant -> Pp.t
+val pr_pinductive          : env -> pinductive -> Pp.t
+val pr_pconstructor        : env -> pconstructor -> Pp.t
 
 
 (** Contexts *)
@@ -122,29 +121,29 @@ val pr_pconstructor        : env -> pconstructor -> std_ppcmds
 val set_compact_context : bool -> unit
 val get_compact_context : unit -> bool
 
-val pr_context_unlimited   : env -> evar_map -> std_ppcmds
-val pr_ne_context_of       : std_ppcmds -> env -> evar_map -> std_ppcmds
+val pr_context_unlimited   : env -> evar_map -> Pp.t
+val pr_ne_context_of       : Pp.t -> env -> evar_map -> Pp.t
 
-val pr_named_decl          : env -> evar_map -> Context.Named.Declaration.t -> std_ppcmds
-val pr_compacted_decl      : env -> evar_map -> Context.Compacted.Declaration.t -> std_ppcmds
-val pr_rel_decl            : env -> evar_map -> Context.Rel.Declaration.t -> std_ppcmds
+val pr_named_decl          : env -> evar_map -> Context.Named.Declaration.t -> Pp.t
+val pr_compacted_decl      : env -> evar_map -> Context.Compacted.Declaration.t -> Pp.t
+val pr_rel_decl            : env -> evar_map -> Context.Rel.Declaration.t -> Pp.t
 
-val pr_named_context       : env -> evar_map -> Context.Named.t -> std_ppcmds
-val pr_named_context_of    : env -> evar_map -> std_ppcmds
-val pr_rel_context         : env -> evar_map -> Context.Rel.t -> std_ppcmds
-val pr_rel_context_of      : env -> evar_map -> std_ppcmds
-val pr_context_of          : env -> evar_map -> std_ppcmds
+val pr_named_context       : env -> evar_map -> Context.Named.t -> Pp.t
+val pr_named_context_of    : env -> evar_map -> Pp.t
+val pr_rel_context         : env -> evar_map -> Context.Rel.t -> Pp.t
+val pr_rel_context_of      : env -> evar_map -> Pp.t
+val pr_context_of          : env -> evar_map -> Pp.t
 
 (** Predicates *)
 
-val pr_predicate           : ('a -> std_ppcmds) -> (bool * 'a list) -> std_ppcmds
-val pr_cpred               : Cpred.t -> std_ppcmds
-val pr_idpred              : Id.Pred.t -> std_ppcmds
-val pr_transparent_state   : transparent_state -> std_ppcmds
+val pr_predicate           : ('a -> Pp.t) -> (bool * 'a list) -> Pp.t
+val pr_cpred               : Cpred.t -> Pp.t
+val pr_idpred              : Id.Pred.t -> Pp.t
+val pr_transparent_state   : transparent_state -> Pp.t
 
 (** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *)
 
-val pr_goal                : goal sigma -> std_ppcmds
+val pr_goal                : goal sigma -> Pp.t
 
 (** [pr_subgoals ~pr_first pp sigma seeds shelf focus_stack unfocused goals]
    prints the goals of the list [goals] followed by the goals in
@@ -155,25 +154,25 @@ val pr_goal                : goal sigma -> std_ppcmds
    focused goals unless the conrresponding option
    [enable_unfocused_goal_printing] is set. [seeds] is for printing
    dependent evars (mainly for emacs proof tree mode). *)
-val pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list
-                             -> goal list -> goal list -> std_ppcmds
+val pr_subgoals            : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list
+                             -> goal list -> goal list -> Pp.t
 
-val pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds
-val pr_concl               : int -> evar_map -> goal -> std_ppcmds
+val pr_subgoal             : int -> evar_map -> goal list -> Pp.t
+val pr_concl               : int -> evar_map -> goal -> Pp.t
 
-val pr_open_subgoals       : ?proof:Proof.proof -> unit -> std_ppcmds
-val pr_nth_open_subgoal    : int -> std_ppcmds
-val pr_evar                : evar_map -> (evar * evar_info) -> std_ppcmds
-val pr_evars_int           : evar_map -> int -> evar_info Evar.Map.t -> std_ppcmds
-val pr_evars               : evar_map -> evar_info Evar.Map.t -> std_ppcmds
-val pr_ne_evar_set         : std_ppcmds -> std_ppcmds -> evar_map ->
-  Evar.Set.t -> std_ppcmds
+val pr_open_subgoals       : ?proof:Proof.proof -> unit -> Pp.t
+val pr_nth_open_subgoal    : int -> Pp.t
+val pr_evar                : evar_map -> (evar * evar_info) -> Pp.t
+val pr_evars_int           : evar_map -> int -> evar_info Evar.Map.t -> Pp.t
+val pr_evars               : evar_map -> evar_info Evar.Map.t -> Pp.t
+val pr_ne_evar_set         : Pp.t -> Pp.t -> evar_map ->
+  Evar.Set.t -> Pp.t
 
-val pr_prim_rule           : prim_rule -> std_ppcmds
+val pr_prim_rule           : prim_rule -> Pp.t
 
 (** Backwards compatibility *)
 
-val prterm                 : constr -> std_ppcmds (** = pr_lconstr *)
+val prterm                 : constr -> Pp.t (** = pr_lconstr *)
 
 
 (** Declarations for the "Print Assumption" command *)
@@ -193,15 +192,15 @@ module ContextObjectMap : CMap.ExtS
   with type key = context_object and module Set := ContextObjectSet
 
 val pr_assumptionset :
-  env -> Term.types ContextObjectMap.t -> std_ppcmds
+  env -> Term.types ContextObjectMap.t -> Pp.t
 
-val pr_goal_by_id : Id.t -> std_ppcmds
-val pr_goal_by_uid : string -> std_ppcmds
+val pr_goal_by_id : Id.t -> Pp.t
+val pr_goal_by_uid : string -> Pp.t
 
 type printer_pr = {
- pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> std_ppcmds;
- pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
- pr_goal                : goal sigma -> std_ppcmds;
+ pr_subgoals            : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t;
+ pr_subgoal             : int -> evar_map -> goal list -> Pp.t;
+ pr_goal                : goal sigma -> Pp.t;
 };;
 
 val set_printer_pr : printer_pr -> unit
diff --git a/printing/printmod.mli b/printing/printmod.mli
index 81b577453..8c3f0149e 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -6,12 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Names
 
 (** false iff the module is an element of an open module type *)
 val printable_body : DirPath.t -> bool
 
-val pr_mutual_inductive_body : Environ.env -> mutual_inductive -> Declarations.mutual_inductive_body -> std_ppcmds
-val print_module : bool -> module_path -> std_ppcmds
-val print_modtype : module_path -> std_ppcmds
+val pr_mutual_inductive_body : Environ.env -> mutual_inductive -> Declarations.mutual_inductive_body -> Pp.t
+val print_module : bool -> module_path -> Pp.t
+val print_modtype : module_path -> Pp.t