diff options
author | 2017-07-31 15:26:39 +0200 | |
---|---|---|
committer | 2017-07-31 15:26:39 +0200 | |
commit | 2f349829c125ed0e2d55548935e7b90e7719f12e (patch) | |
tree | 2d3003a0072af5ab5f1268c1570b2d83ead70060 /plugins/extraction/common.mli | |
parent | 9a872809b246bb6af0c177d530581f7c0c36583f (diff) | |
parent | e3c247c1d96f39d2c07d120b69598a904b7d9f19 (diff) |
Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead
Diffstat (limited to 'plugins/extraction/common.mli')
-rw-r--r-- | plugins/extraction/common.mli | 23 |
1 files changed, 11 insertions, 12 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 |