deprecate Pp.std_ppcmds type alias

14 files changed, 86 insertions, 84 deletions

diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 8ef11a2cd..3f4e8aa12 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -14,7 +14,7 @@ let push = Backtrace.add_backtrace
 
 (* Errors *)
 
-exception Anomaly of string option * std_ppcmds (* System errors *)
+exception Anomaly of string option * Pp.t (* System errors *)
 
 let _ =
   let pr = function
@@ -33,7 +33,7 @@ let is_anomaly = function
 | Anomaly _ -> true
 | _ -> false
 
-exception UserError of string option * std_ppcmds (* User errors *)
+exception UserError of string option * Pp.t (* User errors *)
 
 let todo s = prerr_string ("TODO: "^s^"\n")
 
@@ -41,7 +41,7 @@ let user_err ?loc ?hdr strm = Loc.raise ?loc (UserError (hdr, strm))
 
 let invalid_arg ?loc s   = Loc.raise ?loc (Invalid_argument s)
 
-exception AlreadyDeclared of std_ppcmds (* for already declared Schemes *)
+exception AlreadyDeclared of Pp.t (* for already declared Schemes *)
 let alreadydeclared pps = raise (AlreadyDeclared(pps))
 
 exception Timeout
diff --git a/lib/cErrors.mli b/lib/cErrors.mli
index ca0838575..f3253979f 100644
--- a/lib/cErrors.mli
+++ b/lib/cErrors.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-open Pp
-
 (** This modules implements basic manipulations of errors for use
     throughout Coq's code. *)
 
@@ -21,10 +19,10 @@ val push : exn -> Exninfo.iexn
  [Anomaly] is used for system errors and [UserError] for the
    user's ones. *)
 
-val make_anomaly : ?label:string -> std_ppcmds -> exn
+val make_anomaly : ?label:string -> Pp.t -> exn
 (** Create an anomaly. *)
 
-val anomaly : ?loc:Loc.t -> ?label:string -> std_ppcmds -> 'a
+val anomaly : ?loc:Loc.t -> ?label:string -> Pp.t -> 'a
 (** Raise an anomaly, with an optional location and an optional
     label identifying the anomaly. *)
 
@@ -33,16 +31,16 @@ val is_anomaly : exn -> bool
     This is mostly provided for compatibility. Please avoid doing specific
     tricks with anomalies thanks to it. See rather [noncritical] below. *)
 
-exception UserError of string option * std_ppcmds
+exception UserError of string option * Pp.t
 (** Main error signaling exception. It carries a header plus a pretty printing
     doc *)
 
-val user_err : ?loc:Loc.t -> ?hdr:string -> std_ppcmds -> 'a
+val user_err : ?loc:Loc.t -> ?hdr:string -> Pp.t -> 'a
 (** Main error raising primitive. [user_err ?loc ?hdr pp] signals an
     error [pp] with optional header and location [hdr] [loc] *)
 
-exception AlreadyDeclared of std_ppcmds
-val alreadydeclared : std_ppcmds -> 'a
+exception AlreadyDeclared of Pp.t
+val alreadydeclared : Pp.t -> 'a
 
 val invalid_arg : ?loc:Loc.t -> string -> 'a
 
@@ -74,16 +72,16 @@ exception Quit
 
 exception Unhandled
 
-val register_handler : (exn -> Pp.std_ppcmds) -> unit
+val register_handler : (exn -> Pp.t) -> unit
 
 (** The standard exception printer *)
-val print : ?info:Exninfo.info -> exn -> Pp.std_ppcmds
-val iprint : Exninfo.iexn -> Pp.std_ppcmds
+val print : ?info:Exninfo.info -> exn -> Pp.t
+val iprint : Exninfo.iexn -> Pp.t
 
 (** Same as [print], except that the "Please report" part of an anomaly
     isn't printed (used in Ltac debugging). *)
-val print_no_report : exn -> Pp.std_ppcmds
-val iprint_no_report : Exninfo.iexn -> Pp.std_ppcmds
+val print_no_report : exn -> Pp.t
+val iprint_no_report : Exninfo.iexn -> Pp.t
 
 (** Critical exceptions should not be caught and ignored by mistake
     by inner functions during a [vernacinterp]. They should be handled
@@ -100,9 +98,9 @@ val handled : exn -> bool
 val error : string -> 'a
  [@@ocaml.deprecated "use [user_err] instead"]
 
-val errorlabstrm : string -> std_ppcmds -> 'a
+val errorlabstrm : string -> Pp.t -> 'a
  [@@ocaml.deprecated "use [user_err ~hdr] instead"]
 
-val user_err_loc : Loc.t * string * std_ppcmds -> 'a
+val user_err_loc : Loc.t * string * Pp.t -> 'a
  [@@ocaml.deprecated "use [user_err ~loc] instead"]
 
diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli
index 0622d7593..ba152a19b 100644
--- a/lib/cWarnings.mli
+++ b/lib/cWarnings.mli
@@ -11,7 +11,7 @@ type status = Disabled | Enabled | AsError
 val set_current_loc : Loc.t option -> unit
 
 val create : name:string -> category:string -> ?default:status ->
-             ('a -> Pp.std_ppcmds) -> ?loc:Loc.t -> 'a -> unit
+             ('a -> Pp.t) -> ?loc:Loc.t -> 'a -> unit
 
 val get_flags : unit -> string
 val set_flags : string -> unit
diff --git a/lib/explore.ml b/lib/explore.ml
index 1919af51e..7da077e96 100644
--- a/lib/explore.ml
+++ b/lib/explore.ml
@@ -14,7 +14,7 @@ module type SearchProblem = sig
   type state
   val branching : state -> state list
   val success : state -> bool
-  val pp : state -> std_ppcmds
+  val pp : state -> Pp.t
 end
 
 module Make = functor(S : SearchProblem) -> struct
diff --git a/lib/explore.mli b/lib/explore.mli
index 3c31d0766..5875246ff 100644
--- a/lib/explore.mli
+++ b/lib/explore.mli
@@ -27,7 +27,7 @@ module type SearchProblem = sig
 
   val success : state -> bool
 
-  val pp : state -> Pp.std_ppcmds
+  val pp : state -> Pp.t
 
 end
 
diff --git a/lib/feedback.ml b/lib/feedback.ml
index ed1d495d7..54d16a9be 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -32,7 +32,7 @@ type feedback_content =
   (* Extra metadata *)
   | Custom of Loc.t option * string * xml
   (* Generic messages *)
-  | Message of level * Loc.t option * Pp.std_ppcmds
+  | Message of level * Loc.t option * Pp.t
 
 type feedback = {
   id       : Stateid.t;
diff --git a/lib/feedback.mli b/lib/feedback.mli
index bd3316abb..45a02d384 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -40,7 +40,7 @@ type feedback_content =
   (* Extra metadata *)
   | Custom of Loc.t option * string * xml
   (* Generic messages *)
-  | Message of level * Loc.t option * Pp.std_ppcmds
+  | Message of level * Loc.t option * Pp.t
 
 type feedback = {
   id       : Stateid.t;         (* The document part concerned *)
@@ -78,20 +78,20 @@ relaxed. *)
 (* Should we advertise these functions more? Should they be the ONLY
    allowed way to output something? *)
 
-val msg_info : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+val msg_info : ?loc:Loc.t -> Pp.t -> unit
 (** Message that displays information, usually in verbose mode, such as [Foobar
     is defined] *)
 
-val msg_notice : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+val msg_notice : ?loc:Loc.t -> Pp.t -> unit
 (** Message that should be displayed, such as [Print Foo] or [Show Bar]. *)
 
-val msg_warning : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+val msg_warning : ?loc:Loc.t -> Pp.t -> unit
 (** Message indicating that something went wrong, but without serious
     consequences. *)
 
-val msg_error : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+val msg_error : ?loc:Loc.t -> Pp.t -> unit
 (** Message indicating that something went really wrong, though still
     recoverable; otherwise an exception would have been raised. *)
 
-val msg_debug : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+val msg_debug : ?loc:Loc.t -> Pp.t -> unit
 (** For debugging purposes *)
diff --git a/lib/future.mli b/lib/future.mli
index ce9155657..acfce51a0 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -154,7 +154,7 @@ val purify : ('a -> 'b) -> 'a -> 'b
 val transactify : ('a -> 'b) -> 'a -> 'b
 
 (** Debug: print a computation given an inner printing function. *)
-val print : ('a -> Pp.std_ppcmds) -> 'a computation -> Pp.std_ppcmds
+val print : ('a -> Pp.t) -> 'a computation -> Pp.t
 
 type freeze
 (* These functions are needed to get rid of side effects.
@@ -162,5 +162,5 @@ type freeze
    deal with the whole system state. *)
 val set_freeze : (unit -> freeze) -> (freeze -> unit) -> unit
 
-val customize_not_ready_msg : (string -> Pp.std_ppcmds) -> unit
-val customize_not_here_msg : (string -> Pp.std_ppcmds) -> unit
+val customize_not_ready_msg : (string -> Pp.t) -> unit
+val customize_not_here_msg : (string -> Pp.t) -> unit
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 1174cfe10..b78fe4037 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -58,7 +58,7 @@ fun t1 t2 -> match t1, t2 with
   end
 | _ -> None
 
-let rec pr_genarg_type : type a b c. (a, b, c) genarg_type -> std_ppcmds = function
+let rec pr_genarg_type : type a b c. (a, b, c) genarg_type -> Pp.t = function
 | ListArg t -> pr_genarg_type t ++ spc () ++ str "list"
 | OptArg t -> pr_genarg_type t ++ spc () ++ str "opt"
 | PairArg (t1, t2) ->
diff --git a/lib/genarg.mli b/lib/genarg.mli
index d7f24eac1..7fa71299e 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -146,7 +146,7 @@ val abstract_argument_type_eq :
   ('a, 'l) abstract_argument_type -> ('b, 'l) abstract_argument_type ->
   ('a, 'b) CSig.eq option
 
-val pr_argument_type : argument_type -> Pp.std_ppcmds
+val pr_argument_type : argument_type -> Pp.t
 (** Print a human-readable representation for a given type. *)
 
 val genarg_tag : 'a generic_argument -> argument_type
diff --git a/lib/pp.ml b/lib/pp.ml
index eccaa0928..88ddcb35b 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -39,7 +39,9 @@ type doc_view =
 (* Following discussion on #390, we play on the safe side and make the
    internal representation opaque here. *)
 type t = doc_view
+
 type std_ppcmds = t
+[@@ocaml.deprecated "alias of Pp.t"]
 
 let repr x = x
 let unrepr x = x
diff --git a/lib/pp.mli b/lib/pp.mli
index 96656c8b6..2d11cad86 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -10,7 +10,7 @@
 
 (** Pretty printing guidelines ******************************************)
 (*                                                                      *)
-(* `Pp.t` or `Pp.std_ppcmds` is the main pretty printing document type  *)
+(* `Pp.t` is the main pretty printing document type                     *)
 (* in the Coq system. Documents are composed laying out boxes, and      *)
 (* users can add arbitrary tag metadata that backends are free          *)
 (* to interpret.                                                        *)
@@ -39,7 +39,9 @@ type pp_tag = string
 (* Following discussion on #390, we play on the safe side and make the
    internal representation opaque here. *)
 type t
+
 type std_ppcmds = t
+[@@ocaml.deprecated "alias of Pp.t"]
 
 type block_type =
   | Pp_hbox   of int
@@ -58,127 +60,127 @@ type doc_view =
   | Ppcmd_force_newline
   | Ppcmd_comment of string list
 
-val repr   : std_ppcmds -> doc_view
-val unrepr : doc_view -> std_ppcmds
+val repr   : t -> doc_view
+val unrepr : doc_view -> t
 
 (** {6 Formatting commands} *)
 
-val str   : string -> std_ppcmds
-val brk   : int * int -> std_ppcmds
-val fnl   : unit -> std_ppcmds
-val ws    : int -> std_ppcmds
-val mt    : unit -> std_ppcmds
-val ismt  : std_ppcmds -> bool
+val str   : string -> t
+val brk   : int * int -> t
+val fnl   : unit -> t
+val ws    : int -> t
+val mt    : unit -> t
+val ismt  : t -> bool
 
-val comment  : string list -> std_ppcmds
+val comment  : string list -> t
 
 (** {6 Manipulation commands} *)
 
-val app : std_ppcmds -> std_ppcmds -> std_ppcmds
+val app : t -> t -> t
 (** Concatenation. *)
 
-val seq : std_ppcmds list -> std_ppcmds
+val seq : t list -> t
 (** Multi-Concatenation. *)
 
-val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds
+val (++) : t -> t -> t
 (** Infix alias for [app]. *)
 
 (** {6 Derived commands} *)
 
-val spc : unit -> std_ppcmds
-val cut : unit -> std_ppcmds
-val align : unit -> std_ppcmds
-val int : int -> std_ppcmds
-val real : float -> std_ppcmds
-val bool : bool -> std_ppcmds
-val qstring : string -> std_ppcmds
-val qs : string -> std_ppcmds
-val quote : std_ppcmds -> std_ppcmds
-val strbrk : string -> std_ppcmds
+val spc : unit -> t
+val cut : unit -> t
+val align : unit -> t
+val int : int -> t
+val real : float -> t
+val bool : bool -> t
+val qstring : string -> t
+val qs : string -> t
+val quote : t -> t
+val strbrk : string -> t
 
 (** {6 Boxing commands} *)
 
-val h : int -> std_ppcmds -> std_ppcmds
-val v : int -> std_ppcmds -> std_ppcmds
-val hv : int -> std_ppcmds -> std_ppcmds
-val hov : int -> std_ppcmds -> std_ppcmds
+val h : int -> t -> t
+val v : int -> t -> t
+val hv : int -> t -> t
+val hov : int -> t -> t
 
 (** {6 Tagging} *)
 
-val tag : pp_tag -> std_ppcmds -> std_ppcmds
+val tag : pp_tag -> t -> t
 
 (** {6 Printing combinators} *)
 
-val pr_comma : unit -> std_ppcmds
+val pr_comma : unit -> t
 (** Well-spaced comma. *)
 
-val pr_semicolon : unit -> std_ppcmds
+val pr_semicolon : unit -> t
 (** Well-spaced semicolon. *)
 
-val pr_bar : unit -> std_ppcmds
+val pr_bar : unit -> t
 (** Well-spaced pipe bar. *)
 
-val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds
+val pr_arg : ('a -> t) -> 'a -> t
 (** Adds a space in front of its argument. *)
 
-val pr_non_empty_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds
+val pr_non_empty_arg : ('a -> t) -> 'a -> t
 (** Adds a space in front of its argument if non empty. *)
 
-val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
+val pr_opt : ('a -> t) -> 'a option -> t
 (** Inner object preceded with a space if [Some], nothing otherwise. *)
 
-val pr_opt_no_spc : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
+val pr_opt_no_spc : ('a -> t) -> 'a option -> t
 (** Same as [pr_opt] but without the leading space. *)
 
-val pr_nth : int -> std_ppcmds
+val pr_nth : int -> t
 (** Ordinal number with the correct suffix (i.e. "st", "nd", "th", etc.). *)
 
-val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+val prlist : ('a -> t) -> 'a list -> t
 (** Concatenation of the list contents, without any separator.
 
     Unlike all other functions below, [prlist] works lazily. If a strict
     behavior is needed, use [prlist_strict] instead. *)
 
-val prlist_strict :  ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+val prlist_strict :  ('a -> t) -> 'a list -> t
 (** Same as [prlist], but strict. *)
 
 val prlist_with_sep :
-   (unit -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+   (unit -> t) -> ('a -> t) -> 'a list -> t
 (** [prlist_with_sep sep pr [a ; ... ; c]] outputs
     [pr a ++ sep () ++ ... ++ sep () ++ pr c]. 
     where the thunk sep is memoized, rather than being called each place 
      its result is used.
 *)
 
-val prvect : ('a -> std_ppcmds) -> 'a array -> std_ppcmds
+val prvect : ('a -> t) -> 'a array -> t
 (** As [prlist], but on arrays. *)
 
-val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
+val prvecti : (int -> 'a -> t) -> 'a array -> t
 (** Indexed version of [prvect]. *)
 
 val prvect_with_sep :
-   (unit -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a array -> std_ppcmds
+   (unit -> t) -> ('a -> t) -> 'a array -> t
 (** As [prlist_with_sep], but on arrays. *)
 
 val prvecti_with_sep :
-   (unit -> std_ppcmds) -> (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
+   (unit -> t) -> (int -> 'a -> t) -> 'a array -> t
 (** Indexed version of [prvect_with_sep]. *)
 
-val pr_enum : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+val pr_enum : ('a -> t) -> 'a list -> t
 (** [pr_enum pr [a ; b ; ... ; c]] outputs
     [pr a ++ str "," ++ pr b ++ str "," ++ ... ++ str "and" ++ pr c]. *)
 
-val pr_sequence : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+val pr_sequence : ('a -> t) -> 'a list -> t
 (** Sequence of objects separated by space (unless an element is empty). *)
 
-val surround : std_ppcmds -> std_ppcmds
+val surround : t -> t
 (** Surround with parenthesis. *)
 
-val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
+val pr_vertical_list : ('b -> t) -> 'b list -> t
 
 (** {6 Main renderers, to formatter and to string } *)
 
 (** [pp_with fmt pp] Print [pp] to [fmt] and don't flush [fmt]  *)
-val pp_with          : Format.formatter -> std_ppcmds -> unit
+val pp_with          : Format.formatter -> t -> unit
 
-val string_of_ppcmds : std_ppcmds -> string
+val string_of_ppcmds : t -> string
diff --git a/lib/rtree.mli b/lib/rtree.mli
index a1b06f38e..1a916bbaf 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -78,7 +78,7 @@ val map : ('a -> 'b) -> 'a t -> 'b t
 val smartmap : ('a -> 'a) -> 'a t -> 'a t
 
 (** A rather simple minded pretty-printer *)
-val pp_tree : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
+val pp_tree : ('a -> Pp.t) -> 'a t -> Pp.t
 
 val eq_rtree : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
 (** @deprecated Same as [Rtree.equal] *)
diff --git a/lib/system.mli b/lib/system.mli
index 5f800f191..7281de97c 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -96,7 +96,7 @@ type time
 
 val get_time : unit -> time
 val time_difference : time -> time -> float (** in seconds *)
-val fmt_time_difference : time -> time -> Pp.std_ppcmds
+val fmt_time_difference : time -> time -> Pp.t
 
 val with_time : bool -> ('a -> 'b) -> 'a -> 'b