diff options
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 60c111370..7a80f9121 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -24,8 +24,8 @@ exception Elimconst type 'a stack_member = | Zapp of 'a list - | Zcase of case_info * 'a * 'a array - | Zfix of fixpoint * 'a list + | Zcase of case_info * 'a * 'a array * ('a * 'a list) option + | Zfix of fixpoint * 'a list * ('a * 'a list) option | Zshift of int | Zupdate of 'a @@ -46,7 +46,7 @@ val list_of_app_stack : 'a stack -> 'a list option val array_of_app_stack : 'a stack -> 'a array option val stack_assign : 'a stack -> int -> 'a -> 'a stack val stack_args_size : 'a stack -> int -val zip : constr * constr stack -> constr +val zip : ?refold:bool -> constr * constr stack -> constr val stack_tail : int -> 'a stack -> 'a stack val stack_nth : 'a stack -> int -> 'a @@ -80,6 +80,13 @@ val stack_reduction_of_reduction : i*) val stacklam : (state -> 'a) -> constr list -> constr -> constr stack -> 'a +val whd_state_gen : ?refold:bool -> + Closure.RedFlags.reds -> + Environ.env -> + Evd.evar_map -> + Term.constr * Term.constr stack_member list -> + Term.constr * Term.constr stack_member list + (** {6 Generic Optimized Reduction Function using Closures } *) val clos_norm_flags : Closure.RedFlags.reds -> reduction_function @@ -180,7 +187,7 @@ val is_arity : env -> evar_map -> constr -> bool val whd_programs : reduction_function -val contract_fix : fixpoint -> Term.constr +val contract_fix : fixpoint -> (constr * constr list) option -> constr val fix_recarg : fixpoint -> constr stack -> (int * constr) option (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *) |