diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 21:54:48 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-14 19:17:49 +0100 |
| commit | 539a62a79f75f9f5190b9bd8edfbb04b880a5f1f (patch) | |
| tree | edaa4550ccc2931682f5a4a8ec038f34630da409 /plugins/ssr | |
| parent | 30746e6a9a3296c1aacb2fc03e1c16014232219f (diff) | |
Deprecate dead option Match Strict (ssr).
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 6 |
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 *) |