From e3c247c1d96f39d2c07d120b69598a904b7d9f19 Mon Sep 17 00:00:00 2001
From: Matej Košík <matej.kosik@inria.fr>
Date: Sun, 11 Jun 2017 15:14:15 +0200
Subject: deprecate Pp.std_ppcmds type alias

---
 plugins/extraction/common.mli      | 23 +++++++++++------------
 plugins/extraction/extract_env.mli |  2 +-
 plugins/extraction/miniml.mli      | 15 +++++++--------
 plugins/extraction/table.mli       |  4 ++--
 4 files changed, 21 insertions(+), 23 deletions(-)

(limited to 'plugins/extraction')

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
 
 
 
-- 
cgit v1.2.3