aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
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/funind
parenta960c4db9ae93a6445f9db620f96f62b397ba8b5 (diff)
deprecate Pp.std_ppcmds type alias
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/indfun.mli4
-rw-r--r--plugins/funind/indfun_common.mli9
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 *)