diff options
| author | Gaëtan Gilbert | 2020-02-04 17:07:34 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-12 16:23:49 +0100 |
| commit | 4563779bf990cf22d88474a68acf4eb9cfd8d173 (patch) | |
| tree | c5333864070ccc9b8746799e9236ba90ef1a432d /plugins/ssr/ssrparser.mlg | |
| parent | 6c1de3455d5cd79958a8e26ac728f7d5d1b8d025 (diff) | |
Remove Goptions.opt_name field
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
Diffstat (limited to 'plugins/ssr/ssrparser.mlg')
| -rw-r--r-- | plugins/ssr/ssrparser.mlg | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 22325f3fc3..21b832a326 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -1662,8 +1662,7 @@ let ssr_reserved_ids = Summary.ref ~name:"SSR:idents" true let () = Goptions.(declare_bool_option - { optname = "ssreflect identifiers"; - optkey = ["SsrIdents"]; + { optkey = ["SsrIdents"]; optdepr = false; optread = (fun _ -> !ssr_reserved_ids); optwrite = (fun b -> ssr_reserved_ids := b) @@ -2395,8 +2394,7 @@ let ssr_rw_syntax = Summary.ref ~name:"SSR:rewrite" true let () = Goptions.(declare_bool_option - { optname = "ssreflect rewrite"; - optkey = ["SsrRewrite"]; + { optkey = ["SsrRewrite"]; optread = (fun _ -> !ssr_rw_syntax); optdepr = false; optwrite = (fun b -> ssr_rw_syntax := b) }) |