diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 15:11:52 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 15:11:52 +0100 |
| commit | 0b3a458ecf2cfbe8cd2905d28f2459bd16240a18 (patch) | |
| tree | e49f0cb970aad0ba8dd22088bf51d7d75ce2b8b8 /pretyping | |
| parent | d04f262f4c27a086b9ddfef1931586ef1062614d (diff) | |
| parent | 67091e1d155be19333c5e5bd2cc306792ca630d3 (diff) | |
Merge PR #6895: [compat] Remove "Refolding Reduction" option.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 17 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 5 |
2 files changed, 2 insertions, 20 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index e8b19f6bc..44a69d1c1 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -29,19 +29,6 @@ exception Elimconst their parameters in its stack. *) -let refolding_in_reduction = ref false -let _ = Goptions.declare_bool_option { - Goptions.optdepr = true; (* remove in 8.8 *) - Goptions.optname = - "Perform refolding of fixpoints/constants like cbn during reductions"; - Goptions.optkey = ["Refolding";"Reduction"]; - Goptions.optread = (fun () -> !refolding_in_reduction); - Goptions.optwrite = (fun a -> refolding_in_reduction:=a); -} - -let get_refolding_in_reduction () = !refolding_in_reduction -let set_refolding_in_reduction = (:=) refolding_in_reduction - (** Support for reduction effects *) open Mod_subst @@ -1135,7 +1122,7 @@ let local_whd_state_gen flags sigma = whrec let raw_whd_state_gen flags env = - let f sigma s = fst (whd_state_gen ~refold:(get_refolding_in_reduction ()) + let f sigma s = fst (whd_state_gen ~refold:false ~tactic_mode:false flags env sigma s) in f @@ -1561,7 +1548,7 @@ let is_sort env sigma t = of case/fix (heuristic used by evar_conv) *) let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = - let refold = get_refolding_in_reduction () in + let refold = false in let tactic_mode = false in let rec whrec csts s = let (t, stack as s),csts' = whd_state_gen ~csts ~refold ~tactic_mode CClosure.betaiota env sigma s in diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 3b56513f5..29dc3ed0f 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -31,11 +31,6 @@ module ReductionBehaviour : sig val print : Globnames.global_reference -> Pp.t 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 Support for reduction effects } *) type effect_name = string |