diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/common.mli | 23 | ||||
| -rw-r--r-- | plugins/extraction/extract_env.mli | 2 | ||||
| -rw-r--r-- | plugins/extraction/miniml.mli | 15 | ||||
| -rw-r--r-- | plugins/extraction/table.mli | 4 |
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 |