aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/topconstr.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-10-12 21:14:07 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-10-12 21:14:07 +0200
commit05ad4f49ac2203dd64dfec79a1fc62ee52115724 (patch)
tree920faae7946821c093345fd1804c40336bd9f1c4 /interp/topconstr.ml
parent8a6c792505160de4ba2123ef049ab45d28873e47 (diff)
parent0222f685ebdd55a1596d6689b96ebb86454ba1a7 (diff)
Merge branch 'v8.6'
Diffstat (limited to 'interp/topconstr.ml')
-rw-r--r--interp/topconstr.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index eb564f3b3..b455381ea 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -22,8 +22,7 @@ open Constrexpr_ops
let asymmetric_patterns = ref (false)
let _ = Goptions.declare_bool_option {
Goptions.optsync = true; Goptions.optdepr = false;
- Goptions.optname =
- "Constructors in patterns require all their arguments but no parameters instead of explicit parameters and arguments";
+ Goptions.optname = "no parameters in constructors";
Goptions.optkey = ["Asymmetric";"Patterns"];
Goptions.optread = (fun () -> !asymmetric_patterns);
Goptions.optwrite = (fun a -> asymmetric_patterns:=a);