From e3c247c1d96f39d2c07d120b69598a904b7d9f19 Mon Sep 17 00:00:00 2001 From: Matej Košík Date: Sun, 11 Jun 2017 15:14:15 +0200 Subject: deprecate Pp.std_ppcmds type alias --- plugins/funind/indfun.mli | 4 ++-- plugins/funind/indfun_common.mli | 9 ++++----- 2 files changed, 6 insertions(+), 7 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 7a60da44f..93e03852e 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -1,8 +1,8 @@ open Misctypes -val warn_cannot_define_graph : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit +val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit -val warn_cannot_define_principle : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit +val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit val do_generate_principle : bool -> diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 5e425cd18..2e2ced790 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -1,5 +1,4 @@ open Names -open Pp (* The mk_?_id function build different name w.r.t. a function @@ -11,7 +10,7 @@ val mk_complete_id : Id.t -> Id.t val mk_equation_id : Id.t -> Id.t -val msgnl : std_ppcmds -> unit +val msgnl : Pp.t -> unit val fresh_id : Id.t list -> string -> Id.t val fresh_name : Id.t list -> string -> Name.t @@ -24,7 +23,7 @@ val id_of_name : Name.t -> Id.t val locate_ind : Libnames.reference -> inductive val locate_constant : Libnames.reference -> Constant.t val locate_with_msg : - Pp.std_ppcmds -> (Libnames.reference -> 'a) -> + Pp.t -> (Libnames.reference -> 'a) -> Libnames.reference -> 'a val filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list @@ -89,8 +88,8 @@ val update_Function : function_info -> unit (** debugging *) -val pr_info : function_info -> Pp.std_ppcmds -val pr_table : unit -> Pp.std_ppcmds +val pr_info : function_info -> Pp.t +val pr_table : unit -> Pp.t (* val function_debug : bool ref *) -- cgit v1.2.3