deprecate Pp.std_ppcmds type alias

10 files changed, 18 insertions, 18 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 3eb5b0753..364fc883b 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -58,7 +58,7 @@ module SentenceId : sig
   val connect : sentence -> signals
 
   val dbg_to_string :
-    GText.buffer -> bool -> Stateid.t option -> sentence -> Pp.std_ppcmds
+    GText.buffer -> bool -> Stateid.t option -> sentence -> Pp.t
 
 end = struct
 
@@ -163,7 +163,7 @@ let flags_to_color f =
   else `NAME Preferences.processed_color#get
 
 (* Move to utils? *)
-let rec validate (s : Pp.std_ppcmds) = match Pp.repr s with
+let rec validate (s : Pp.t) = match Pp.repr s with
   | Pp.Ppcmd_empty
   | Pp.Ppcmd_print_break _
   | Pp.Ppcmd_force_newline  -> true
diff --git a/ide/document.mli b/ide/document.mli
index fb96cb6d7..ab8e71808 100644
--- a/ide/document.mli
+++ b/ide/document.mli
@@ -102,7 +102,7 @@ val context : 'a document -> (id * 'a) list * (id * 'a) list
 
 (** debug print *)
 val print :
-  'a document -> (bool -> id option -> 'a ->  Pp.std_ppcmds) -> Pp.std_ppcmds
+  'a document -> (bool -> id option -> 'a ->  Pp.t) -> Pp.t
 
 (** Callbacks on documents *)
 
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 2573b6d6f..83e5da950 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -316,7 +316,7 @@ let textview_width (view : #GText.view_skel) =
   let char_width = GPango.to_pixels metrics#approx_char_width in
   pixel_width / char_width
 
-type logger = Feedback.level -> Pp.std_ppcmds -> unit
+type logger = Feedback.level -> Pp.t -> unit
 
 let default_logger level message =
   let level = match level with
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 458b8e0a5..f06a48aeb 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -67,7 +67,7 @@ val requote : string -> string
 val textview_width : #GText.view_skel -> int
 (** Returns an approximate value of the character width of a textview *)
 
-type logger = Feedback.level -> Pp.std_ppcmds -> unit
+type logger = Feedback.level -> Pp.t -> unit
 
 val default_logger : logger
 (** Default logger. It logs messages that the casual user should not see. *)
diff --git a/ide/interface.mli b/ide/interface.mli
index aab1d8272..1939a8427 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -17,9 +17,9 @@ type verbose = bool
 type goal = {
   goal_id : string;
   (** Unique goal identifier *)
-  goal_hyp : Pp.std_ppcmds list;
+  goal_hyp : Pp.t list;
   (** List of hypotheses *)
-  goal_ccl : Pp.std_ppcmds;
+  goal_ccl : Pp.t;
   (** Goal conclusion *)
 }
 
@@ -121,7 +121,7 @@ type edit_id  = int
    should probably retract to that point *)
 type 'a value =
   | Good of 'a
-  | Fail of (state_id * location * Pp.std_ppcmds)
+  | Fail of (state_id * location * Pp.t)
 
 type ('a, 'b) union = ('a, 'b) Util.union
 
@@ -213,7 +213,7 @@ type about_sty = unit
 type about_rty = coq_info
 
 type handle_exn_sty = Exninfo.iexn
-type handle_exn_rty = state_id * location * Pp.std_ppcmds
+type handle_exn_rty = state_id * location * Pp.t
 
 (* Retrocompatibility stuff *)
 type interp_sty = (raw * verbose) * string
diff --git a/ide/minilib.mli b/ide/minilib.mli
index 4517a2374..c96e59b22 100644
--- a/ide/minilib.mli
+++ b/ide/minilib.mli
@@ -22,7 +22,7 @@ type level = [
 (** debug printing *)
 val debug : bool ref
 
-val log_pp : ?level:level -> Pp.std_ppcmds -> unit
+val log_pp : ?level:level -> Pp.t -> unit
 val log    : ?level:level -> string        -> unit
 
 val coqide_config_home : unit -> string
diff --git a/ide/richpp.mli b/ide/richpp.mli
index f2ba15d22..84adc61ca 100644
--- a/ide/richpp.mli
+++ b/ide/richpp.mli
@@ -24,7 +24,7 @@ type 'annotation located = {
     that represents (located) annotations of this string.
     The [get_annotations] function is used to convert tags into the desired
     annotation. [width] sets the printing witdh of the formatter. *)
-val rich_pp : int -> Pp.std_ppcmds -> Pp.pp_tag located Xml_datatype.gxml
+val rich_pp : int -> Pp.t -> Pp.pp_tag located Xml_datatype.gxml
 
 (** [annotations_positions ssdoc] returns a list associating each
     annotations with its position in the string from which [ssdoc] is
@@ -47,5 +47,5 @@ type richpp = Xml_datatype.xml
 
 (** Type of text with style annotations *)
 
-val richpp_of_pp : int -> Pp.std_ppcmds -> richpp
+val richpp_of_pp : int -> Pp.t -> richpp
 (** Extract style information from formatted text *)
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index d2a09dd94..65df2b849 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -28,9 +28,9 @@ class type message_view =
     inherit GObj.widget
     method connect : message_view_signals
     method clear : unit
-    method add : Pp.std_ppcmds -> unit
+    method add : Pp.t -> unit
     method add_string : string -> unit
-    method set : Pp.std_ppcmds -> unit
+    method set : Pp.t -> unit
     method refresh : bool -> unit
     method push : Ideutils.logger
       (** same as [add], but with an explicit level instead of [Notice] *)
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli
index 0ce257c3d..6bd0625f0 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/wg_MessageView.mli
@@ -18,9 +18,9 @@ class type message_view =
     inherit GObj.widget
     method connect : message_view_signals
     method clear : unit
-    method add : Pp.std_ppcmds -> unit
+    method add : Pp.t -> unit
     method add_string : string -> unit
-    method set : Pp.std_ppcmds -> unit
+    method set : Pp.t -> unit
     method refresh : bool -> unit
     method push : Ideutils.logger
       (** same as [add], but with an explicit level instead of [Notice] *)
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 06c695c77..4b521a968 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -117,7 +117,7 @@ let to_box = let open Pp in
       | x        -> raise (Marshal_error("*ppbox",PCData x))
     )
 
-let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match Pp.repr pp with
+let rec of_pp (pp : Pp.t) = let open Pp in match Pp.repr pp with
     | Ppcmd_empty         -> constructor "ppdoc" "empty"  []
     | Ppcmd_string s      -> constructor "ppdoc" "string" [of_string s]
     | Ppcmd_glue sl       -> constructor "ppdoc" "glue"   [of_list of_pp sl]
@@ -149,7 +149,7 @@ let rec to_pp xpp = let open Pp in
 let of_richpp x = Element ("richpp", [], [x])
 
 (* Run-time Selectable *)
-let of_pp (pp : Pp.std_ppcmds) =
+let of_pp (pp : Pp.t) =
   match !msg_format with
   | Richpp margin -> of_richpp (Richpp.richpp_of_pp margin pp)
   | Ppcmds        -> of_pp pp