deprecate Pp.std_ppcmds type alias

1 files changed, 31 insertions, 33 deletions

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