aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/reductionops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index cc1709f1c2..ce9ca93d90 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -29,7 +29,7 @@ exception Elimconst
let refolding_in_reduction = ref false
let _ = Goptions.declare_bool_option {
- Goptions.optdepr = false;
+ Goptions.optdepr = true; (* remove in 8.8 *)
Goptions.optname =
"Perform refolding of fixpoints/constants like cbn during reductions";
Goptions.optkey = ["Refolding";"Reduction"];