diff options
| author |  Matej Košík <matej.kosik@inria.fr> | 2017-06-11 15:14:15 +0200 |
|---|---|---|
| committer | Matej Košík <matej.kosik@inria.fr> | 2017-07-27 10:10:23 +0200 |
| commit | e3c247c1d96f39d2c07d120b69598a904b7d9f19 (patch) | |
| tree | a9d3735d5d3f53140aa1123e87f4d4c8db8840f8 /pretyping/reductionops.mli | |
| parent | a960c4db9ae93a6445f9db620f96f62b397ba8b5 (diff) | |
deprecate Pp.std_ppcmds type alias
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index db407b6c9..1828196fe 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -26,7 +26,7 @@ module ReductionBehaviour : sig bool -> Globnames.global_reference -> (int list * int * flag list) -> unit val get : Globnames.global_reference -> (int list * int * flag list) option - val print : Globnames.global_reference -> Pp.std_ppcmds + val print : Globnames.global_reference -> Pp.t end (** Option telling if reduction should use the refolding machinery of cbn @@ -63,13 +63,13 @@ module Cst_stack : sig val best_cst : t -> (constr * constr list) option val best_replace : Evd.evar_map -> constr -> t -> constr -> constr val reference : Evd.evar_map -> t -> Constant.t option - val pr : t -> Pp.std_ppcmds + val pr : t -> Pp.t end module Stack : sig type 'a app_node - val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds + val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t type cst_member = | Cst_const of pconstant @@ -86,7 +86,7 @@ module Stack : sig | Update of 'a and 'a t = 'a member list - val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds + val pr : ('a -> Pp.t) -> 'a t -> Pp.t val empty : 'a t val is_empty : 'a t -> bool @@ -145,7 +145,7 @@ type contextual_state_reduction_function = type state_reduction_function = contextual_state_reduction_function type local_state_reduction_function = evar_map -> state -> state -val pr_state : state -> Pp.std_ppcmds +val pr_state : state -> Pp.t (** {6 Reduction Function Operators } *) |