aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
diff options
context:
space:
mode:
authorGravatar Matej Košík <matej.kosik@inria.fr>2017-06-11 15:14:15 +0200
committerGravatar Matej Košík <matej.kosik@inria.fr>2017-07-27 10:10:23 +0200
commite3c247c1d96f39d2c07d120b69598a904b7d9f19 (patch)
treea9d3735d5d3f53140aa1123e87f4d4c8db8840f8 /plugins/extraction
parenta960c4db9ae93a6445f9db620f96f62b397ba8b5 (diff)
deprecate Pp.std_ppcmds type alias
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/common.mli23
-rw-r--r--plugins/extraction/extract_env.mli2
-rw-r--r--plugins/extraction/miniml.mli15
-rw-r--r--plugins/extraction/table.mli4
4 files changed, 21 insertions, 23 deletions
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