aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/topconstr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/topconstr.ml')
-rw-r--r--interp/topconstr.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index e05be65fb..239226b2e 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -21,7 +21,7 @@ open Constrexpr_ops
let asymmetric_patterns = ref (false)
let _ = Goptions.declare_bool_option {
- Goptions.optsync = true; Goptions.optdepr = false;
+ Goptions.optdepr = false;
Goptions.optname = "no parameters in constructors";
Goptions.optkey = ["Asymmetric";"Patterns"];
Goptions.optread = (fun () -> !asymmetric_patterns);