From 67091e1d155be19333c5e5bd2cc306792ca630d3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Sat, 3 Mar 2018 01:38:19 +0100
Subject: [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.
---
 pretyping/reductionops.ml  | 17 ++---------------
 pretyping/reductionops.mli |  5 -----
 2 files changed, 2 insertions(+), 20 deletions(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3