Boolean Option Patterns Compatibility

switch between "all arguments no parameters" and "explicit params and args"
for constructor arguments in patterns.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14919 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 0 deletions

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index ab85f8465..0db70e59c 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -916,6 +916,16 @@ and typeclass_context = typeclass_constraint list
 
 type constr_pattern_expr = constr_expr
 
+let oldfashion_patterns = ref (true)
+let write_oldfashion_patterns = Goptions.declare_bool_option {
+  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optname =
+    "Constructors in atterns require all their arguments but no parameters instead of explicit parameters and arguments";
+  Goptions.optkey = ["Asymmetric";"Patterns"];
+  Goptions.optread = (fun () -> !oldfashion_patterns);
+  Goptions.optwrite = (fun a -> oldfashion_patterns:=a);
+}
+
 (***********************)
 (* For binders parsing *)