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 /proofs | |
| 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 'proofs')
| -rw-r--r-- | proofs/goal_select.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_bullet.ml | 1 |
2 files changed, 0 insertions, 2 deletions
diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml index a6e27c238f..36b50d9e9f 100644 --- a/proofs/goal_select.ml +++ b/proofs/goal_select.ml @@ -56,7 +56,6 @@ let parse_goal_selector = function let () = let open Goptions in declare_string_option { optdepr = false; - optname = "default goal selector" ; optkey = ["Default";"Goal";"Selector"] ; optread = begin fun () -> Pp.string_of_ppcmds diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index 61e8741973..3ff0533b6b 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -179,7 +179,6 @@ let current_behavior = ref Strict.strict let () = Goptions.(declare_string_option { optdepr = false; - optname = "bullet behavior"; optkey = ["Bullet";"Behavior"]; optread = begin fun () -> (!current_behavior).name |