aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--plugins/ssr/ssrequality.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index bd9633afb..6032ed2af 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -143,14 +143,14 @@ let newssrcongrtac arg ist gl =
(** Coq rewrite compatibility flag *)
-let ssr_strict_match = ref false
let _ =
- Goptions.declare_bool_option
+ let ssr_strict_match = ref false in
+ Goptions.declare_bool_option
{ Goptions.optname = "strict redex matching";
Goptions.optkey = ["Match"; "Strict"];
Goptions.optread = (fun () -> !ssr_strict_match);
- Goptions.optdepr = false;
+ Goptions.optdepr = true; (* noop *)
Goptions.optwrite = (fun b -> ssr_strict_match := b) }
(** Rewrite rules *)