aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cbv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/cbv.ml')
-rw-r--r--pretyping/cbv.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index bd7350dc4..782552583 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -177,7 +177,7 @@ let cofixp_reducible flgs _ stk =
let debug_cbv = ref false
let _ = Goptions.declare_bool_option {
- Goptions.optsync = true; Goptions.optdepr = false;
+ Goptions.optdepr = false;
Goptions.optname = "cbv visited constants display";
Goptions.optkey = ["Debug";"Cbv"];
Goptions.optread = (fun () -> !debug_cbv);