From 4563779bf990cf22d88474a68acf4eb9cfd8d173 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 4 Feb 2020 17:07:34 +0100
Subject: 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.
---
 proofs/goal_select.ml  | 1 -
 proofs/proof_bullet.ml | 1 -
 2 files changed, 2 deletions(-)

(limited to 'proofs')

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
-- 
cgit v1.2.3