diff options
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 |