aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/reductionops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/reductionops.ml')
-rw-r--r--pretyping/reductionops.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 52f424f75..117ed338e 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.optsync = true; Goptions.optdepr = false;
+ Goptions.optdepr = false;
Goptions.optname =
"Perform refolding of fixpoints/constants like cbn during reductions";
Goptions.optkey = ["Refolding";"Reduction"];
@@ -811,7 +811,7 @@ let fix_recarg ((recindices,bodynum),_) stack =
let debug_RAKAM = ref (false)
let _ = Goptions.declare_bool_option {
- Goptions.optsync = true; Goptions.optdepr = false;
+ Goptions.optdepr = false;
Goptions.optname =
"Print states of the Reductionops abstract machine";
Goptions.optkey = ["Debug";"RAKAM"];