diff options
| author | Emilio Jesus Gallego Arias | 2018-03-03 01:38:19 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-03-08 21:15:33 +0100 |
| commit | 67091e1d155be19333c5e5bd2cc306792ca630d3 (patch) | |
| tree | 04d89c833d37447ee2a02852fb887aedac1edc81 /pretyping/reductionops.ml | |
| parent | 3875a525ee1e075be9f0eb1f17c74726e9f38b43 (diff) | |
[compat] Remove "Refolding Reduction" option.
Following up on #6791, we remove support refolding in reduction.
We also update a test case that was not properly understood, see the
discussion in #6895.
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 17 |
1 files changed, 2 insertions, 15 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index e8b19f6bc4..44a69d1c1e 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 |