diff options
| author |  Paul Steckler <steck@stecksoft.com> | 2016-06-28 12:37:00 -0400 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2016-09-09 18:12:26 +0200 |
| commit | 43869b4e05824244e666c60e0b740a80e8b09d0c (patch) | |
| tree | 119fd8db5cd7bde7750d84fcf107b6ca482aa7fe /pretyping/reductionops.mli | |
| parent | dee69387bd4b2944c9e81ee422fb9900ab0e6c4d (diff) | |
no-refold patch
Add a boolean for refolding during reduction, and an option
that is off by default in 8.6, to turn refolding on in all reduction
functions, as in 8.5.
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 874ea6815..4cd7a2a86 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -28,6 +28,11 @@ module ReductionBehaviour : sig val print : Globnames.global_reference -> Pp.std_ppcmds end +(** Option telling if reduction should use the refolding machinery of cbn + (off by default) *) +val get_refolding_in_reduction : unit -> bool +val set_refolding_in_reduction : bool -> unit + (** {6 Machinery about a stack of unfolded constant } cst applied to params must convertible to term of the state applied to args @@ -134,8 +139,8 @@ val stack_reduction_of_reduction : i*) val stacklam : (state -> 'a) -> constr list -> constr -> constr Stack.t -> 'a -val whd_state_gen : ?csts:Cst_stack.t -> bool -> CClosure.RedFlags.reds -> - Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t +val whd_state_gen : ?csts:Cst_stack.t -> refold:bool -> tactic_mode:bool -> + CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t val iterate_whd_gen : bool -> CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> Term.constr -> Term.constr |