diff options
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 27 |
1 files changed, 15 insertions, 12 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index b8ac085a..c0ff6723 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -25,10 +25,10 @@ module ReductionBehaviour : sig (** [set is_local ref (recargs, nargs, flags)] *) val set : - bool -> Globnames.global_reference -> (int list * int * flag list) -> unit + bool -> GlobRef.t -> (int list * int * flag list) -> unit val get : - Globnames.global_reference -> (int list * int * flag list) option - val print : Globnames.global_reference -> Pp.t + GlobRef.t -> (int list * int * flag list) option + val print : GlobRef.t -> Pp.t end (** {6 Support for reduction effects } *) @@ -41,10 +41,10 @@ val declare_reduction_effect : effect_name -> (Environ.env -> Evd.evar_map -> Constr.constr -> unit) -> unit (* [set_reduction_effect cst name] declares effect [name] to be called when [cst] is found *) -val set_reduction_effect : Globnames.global_reference -> effect_name -> unit +val set_reduction_effect : Constant.t -> effect_name -> unit (* [effect_hook env sigma key term] apply effect associated to [key] on [term] *) -val reduction_effect_hook : Environ.env -> Evd.evar_map -> Constr.constr -> +val reduction_effect_hook : Environ.env -> Evd.evar_map -> Constant.t -> Constr.constr Lazy.t -> unit (** {6 Machinery about a stack of unfolded constant } @@ -60,7 +60,7 @@ 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.t + val pr : env -> Evd.evar_map -> t -> Pp.t end module Stack : sig @@ -75,7 +75,7 @@ module Stack : sig type 'a member = | App of 'a app_node | Case of case_info * 'a * 'a array * Cst_stack.t - | Proj of int * int * Projection.t * Cst_stack.t + | Proj of Projection.t * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int (** current foccussed arg *) * int list (** remaining args *) * 'a t * Cst_stack.t @@ -140,10 +140,13 @@ 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.t +val pr_state : env -> evar_map -> state -> Pp.t (** {6 Reduction Function Operators } *) +val strong_with_flags : + (CClosure.RedFlags.reds -> reduction_function) -> + (CClosure.RedFlags.reds -> reduction_function) val strong : reduction_function -> reduction_function val local_strong : local_reduction_function -> local_reduction_function val strong_prodspine : local_reduction_function -> local_reduction_function @@ -277,13 +280,13 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> con otherwise returns false in that case. *) val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> - env -> evar_map -> constr -> constr -> evar_map * bool + env -> evar_map -> constr -> constr -> evar_map option (** Conversion with inference of universe constraints *) val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> constr -> constr -> - evar_map * bool) -> unit + evar_map option) -> unit val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr -> - evar_map * bool + evar_map option (** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a @@ -291,7 +294,7 @@ conversion function. Used to pretype vm and native casts. *) val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state -> (Constr.constr, evar_map) Reduction.generic_conversion_function) -> ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env -> - evar_map -> constr -> constr -> evar_map * bool + evar_map -> constr -> constr -> evar_map option (** {6 Special-Purpose Reduction Functions } *) |