diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-07-31 15:26:39 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-07-31 15:26:39 +0200 |
| commit | 2f349829c125ed0e2d55548935e7b90e7719f12e (patch) | |
| tree | 2d3003a0072af5ab5f1268c1570b2d83ead70060 /plugins/funind | |
| parent | 9a872809b246bb6af0c177d530581f7c0c36583f (diff) | |
| parent | e3c247c1d96f39d2c07d120b69598a904b7d9f19 (diff) | |
Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/indfun.mli | 4 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.mli | 9 |
2 files changed, 6 insertions, 7 deletions
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 *) |