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.

64 files changed, 33 insertions, 192 deletions

diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index b0197c500c..f706633da9 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -35,6 +35,11 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`,
    use the Simplex method for solving linear goals. If it is not set,
    the decision procedures are using Fourier elimination.
 
+.. opt:: Dump Arith
+
+   This option (unset by default) may be set to a file path where
+   debug info will be written.
+
 .. cmd:: Show Lia Profile
 
    This command prints some statistics about the amount of pivoting
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 56277e8092..bcc8c34a4d 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -216,7 +216,6 @@ let it_mkLambda_or_LetIn_name env sigma b hyps =
 let get_mangle_names =
   Goptions.declare_bool_option_and_ref
     ~depr:false
-    ~name:"mangle auto-generated names"
     ~key:["Mangle";"Names"]
     ~value:false
 
@@ -227,7 +226,6 @@ let set_prefix x = mangle_names_prefix := forget_subscript x
 let () = Goptions.(
     declare_string_option
       { optdepr  = false;
-        optname  = "mangled names prefix";
         optkey   = ["Mangle";"Names";"Prefix"];
         optread  = (fun () -> Id.to_string !mangle_names_prefix);
         optwrite = begin fun x ->
diff --git a/engine/uState.ml b/engine/uState.ml
index 3546ece581..2eaa202246 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -53,7 +53,7 @@ let empty =
     uctx_weak_constraints = UPairSet.empty; }
 
 let elaboration_sprop_cumul =
-  Goptions.declare_bool_option_and_ref ~depr:false ~name:"SProp cumulativity during elaboration"
+  Goptions.declare_bool_option_and_ref ~depr:false
     ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true
 
 let make ~lbound u =
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index fc0770cf75..53ff041fa5 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -15,7 +15,6 @@ open UnivSubst
 let get_set_minimization =
   Goptions.declare_bool_option_and_ref
     ~depr:false
-    ~name:"minimization to Set"
     ~key:["Universe";"Minimization";"ToSet"]
     ~value:true
 
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 7d92cff365..ae2301a0a7 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -360,7 +360,6 @@ let import_option_value = function
 let export_option_state s = {
   Interface.opt_sync  = true;
   Interface.opt_depr  = s.Goptions.opt_depr;
-  Interface.opt_name  = s.Goptions.opt_name;
   Interface.opt_value = export_option_value s.Goptions.opt_value;
 }
 
diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml
index 362833743e..be5e305ad3 100644
--- a/ide/protocol/interface.ml
+++ b/ide/protocol/interface.ml
@@ -71,8 +71,6 @@ type option_state = {
   (** Whether an option is synchronous *)
   opt_depr  : bool;
   (** Whether an option is deprecated *)
-  opt_name  : string;
-  (** A short string that is displayed when using [Test] *)
   opt_value : option_value;
   (** The current value of the option *)
 }
diff --git a/ide/protocol/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml
index cad65cc5d6..a2c80ea118 100644
--- a/ide/protocol/xmlprotocol.ml
+++ b/ide/protocol/xmlprotocol.ml
@@ -79,13 +79,11 @@ let of_option_state s =
   Element ("option_state", [], [
     of_bool s.opt_sync;
     of_bool s.opt_depr;
-    of_string s.opt_name;
     of_option_value s.opt_value])
 let to_option_state = function
-  | Element ("option_state", [], [sync; depr; name; value]) -> {
+  | Element ("option_state", [], [sync; depr; value]) -> {
       opt_sync = to_bool sync;
       opt_depr = to_bool depr;
-      opt_name = to_string name;
       opt_value = to_option_value value }
   | x -> raise (Marshal_error("option_state",x))
 
@@ -429,8 +427,8 @@ end = struct
     | StringOptValue (Some s) -> s
     | BoolValue b -> if b then "true" else "false"
   let pr_option_state (s : option_state) =
-    Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n"
-      s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value)
+    Printf.sprintf "sync := %b; depr := %b; value := %s\n"
+      s.opt_sync s.opt_depr (pr_option_value s.opt_value)
   let pr_list pr l = "["^String.concat ";" (List.map pr l)^"]"
   let pr_option pr = function None -> "None" | Some x -> "Some("^pr x^")"
   let pr_coq_object (o : 'a coq_object) = "FIXME"
@@ -513,7 +511,7 @@ end = struct
                    "type which contains a flattened n-tuple.  We provide one example.\n");
     Printf.printf "%s:\n\n%s\n\n" (print_val_t Option_state)
       (pr_xml (of_option_state { opt_sync = true; opt_depr = false;
-        opt_name = "name1"; opt_value = IntValue (Some 37) }));
+                                 opt_value = IntValue (Some 37) }));
 
 end
 open ReifType
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c55e17e7a3..c198c4eb9b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -194,7 +194,6 @@ let without_specific_symbols l =
 let get_record_print =
   Goptions.declare_bool_option_and_ref
     ~depr:false
-    ~name:"record printing"
     ~key:["Printing";"Records"]
     ~value:true
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2ceea58297..b2c572d290 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1615,7 +1615,6 @@ let is_non_zero_pat c = match c with
 
 let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref
     ~depr:false
-    ~name:"no parameters in constructors"
     ~key:["Asymmetric";"Patterns"]
     ~value:false
 
diff --git a/library/goptions.ml b/library/goptions.ml
index 6e53bed349..616f6edf72 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -27,7 +27,6 @@ type option_value =
 (** Summary of an option status *)
 type option_state = {
   opt_depr  : bool;
-  opt_name  : string;
   opt_value : option_value;
 }
 
@@ -190,7 +189,6 @@ module MakeRefTable =
 
 type 'a option_sig = {
   optdepr  : bool;
-  optname  : string;
   optkey   : option_name;
   optread  : unit -> 'a;
   optwrite : 'a -> unit }
@@ -229,7 +227,7 @@ let warn_deprecated_option =
                        strbrk " is deprecated")
 
 let declare_option cast uncast append ?(preprocess = fun x -> x)
-  { optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
+  { optdepr=depr; optkey=key; optread=read; optwrite=write } =
   check_key key;
   let default = read() in
   let change =
@@ -275,7 +273,7 @@ let declare_option cast uncast append ?(preprocess = fun x -> x)
   let cread () = cast (read ()) in
   let cwrite l v = warn (); change l OptSet (uncast v) in
   let cappend l v = warn (); change l OptAppend (uncast v) in
-  value_tab := OptionMap.add key (name, depr, (cread,cwrite,cappend)) !value_tab
+  value_tab := OptionMap.add key (depr, (cread,cwrite,cappend)) !value_tab
 
 let declare_int_option =
   declare_option
@@ -298,13 +296,12 @@ let declare_stringopt_option =
     (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option."))
     (fun _ _ -> anomaly (Pp.str "async_option."))
 
-let declare_bool_option_and_ref ~depr ~name ~key ~(value:bool) =
+let declare_bool_option_and_ref ~depr ~key ~(value:bool) =
   let r_opt = ref value in
   let optwrite v = r_opt := v in
   let optread () = !r_opt in
   let _ = declare_bool_option {
       optdepr = depr;
-      optname = name;
       optkey = key;
       optread; optwrite
     } in
@@ -323,7 +320,7 @@ let set_option_value ?(locality = OptDefault) check_and_cast key v =
   let opt = try Some (get_option key) with Not_found -> None in
   match opt with
   | None -> warn_unknown_option key
-  | Some (name, depr, (read,write,append)) ->
+  | Some (depr, (read,write,append)) ->
     write locality (check_and_cast v (read ()))
 
 let show_value_type = function
@@ -373,7 +370,7 @@ let set_string_option_append_value_gen ?(locality = OptDefault) key v =
   let opt = try Some (get_option key) with Not_found -> None in
   match opt with
   | None -> warn_unknown_option key
-  | Some (name, depr, (read,write,append)) ->
+  | Some (depr, (read,write,append)) ->
     append locality (check_string_value v (read ()))
 
 let set_int_option_value opt v = set_int_option_value_gen opt v
@@ -382,7 +379,7 @@ let set_string_option_value opt v = set_string_option_value_gen opt v
 
 (* Printing options/tables *)
 
-let msg_option_value (name,v) =
+let msg_option_value v =
   match v with
     | BoolValue true  -> str "on"
     | BoolValue false -> str "off"
@@ -394,19 +391,18 @@ let msg_option_value (name,v) =
 (*     | IdentValue r    -> pr_global_env Id.Set.empty r *)
 
 let print_option_value key =
-  let (name, depr, (read,_,_)) = get_option key in
+  let (depr, (read,_,_)) = get_option key in
   let s = read () in
   match s with
     | BoolValue b ->
-        Feedback.msg_notice (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
+        Feedback.msg_notice (prlist_with_sep spc str key ++ str " is " ++ str (if b then "on" else "off"))
     | _ ->
-        Feedback.msg_notice (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
+        Feedback.msg_notice (str "Current value of " ++ prlist_with_sep spc str key ++ str " is " ++ msg_option_value s)
 
 let get_tables () =
   let tables = !value_tab in
-  let fold key (name, depr, (read,_,_)) accu =
+  let fold key (depr, (read,_,_)) accu =
     let state = {
-      opt_name = name;
       opt_depr = depr;
       opt_value = read ();
     } in
@@ -415,15 +411,15 @@ let get_tables () =
   OptionMap.fold fold tables OptionMap.empty
 
 let print_tables () =
-  let print_option key name value depr =
-    let msg = str "  " ++ str (nickname key) ++ str ": " ++ msg_option_value (name, value) in
+  let print_option key value depr =
+    let msg = str "  " ++ str (nickname key) ++ str ": " ++ msg_option_value value in
     if depr then msg ++ str " [DEPRECATED]" ++ fnl ()
     else msg ++ fnl ()
   in
   str "Options:" ++ fnl () ++
     OptionMap.fold
-      (fun key (name, depr, (read,_,_)) p ->
-        p ++ print_option key name (read ()) depr)
+      (fun key (depr, (read,_,_)) p ->
+        p ++ print_option key (read ()) depr)
       !value_tab (mt ()) ++
   str "Tables:" ++ fnl () ++
     List.fold_right
diff --git a/library/goptions.mli b/library/goptions.mli
index 29af196654..e3791dffb1 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -111,8 +111,6 @@ end
 type 'a option_sig = {
   optdepr    : bool;
   (** whether the option is DEPRECATED *)
-  optname    : string;
-  (** a short string describing the option *)
   optkey     : option_name;
   (** the low-level name of this option *)
   optread    : unit -> 'a;
@@ -133,7 +131,7 @@ val declare_stringopt_option: ?preprocess:(string option -> string option) ->
 
 (** Helper to declare a reference controlled by an option. Read-only
    as to avoid races. *)
-val declare_bool_option_and_ref : depr:bool -> name:string -> key:option_name -> value:bool -> (unit -> bool)
+val declare_bool_option_and_ref : depr:bool -> key:option_name -> value:bool -> (unit -> bool)
 
 (** {6 Special functions supposed to be used only in vernacentries.ml } *)
 
@@ -181,7 +179,6 @@ val set_option_value : ?locality:option_locality ->
 (** Summary of an option status *)
 type option_state = {
   opt_depr  : bool;
-  opt_name  : string;
   opt_value : option_value;
 }
 
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index fdc70ccaa8..f9078c4bdc 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -33,7 +33,6 @@ let debug x =
 let () =
   let gdopt=
     { optdepr=false;
-      optname="Congruence Verbose";
       optkey=["Congruence";"Verbose"];
       optread=(fun ()-> !cc_verbose);
       optwrite=(fun b -> cc_verbose := b)}
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 7b64706138..9d07cd7d93 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -503,7 +503,6 @@ let my_bool_option name initval =
   let access = fun () -> !flag in
   let () = declare_bool_option
     {optdepr = false;
-     optname = "Extraction "^name;
      optkey = ["Extraction"; name];
      optread = access;
      optwrite = (:=) flag }
@@ -575,14 +574,12 @@ let optims () = !opt_flag_ref
 
 let () = declare_bool_option
           {optdepr = false;
-           optname = "Extraction Optimize";
            optkey = ["Extraction"; "Optimize"];
            optread = (fun () -> not (Int.equal !int_flag_ref 0));
            optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))}
 
 let () = declare_int_option
           { optdepr = false;
-            optname = "Extraction Flag";
             optkey = ["Extraction";"Flag"];
             optread = (fun _ -> Some !int_flag_ref);
             optwrite = (function
@@ -596,7 +593,6 @@ let conservative_types () = !conservative_types_ref
 
 let () = declare_bool_option
   {optdepr = false;
-   optname = "Extraction Conservative Types";
    optkey = ["Extraction"; "Conservative"; "Types"];
    optread = (fun () -> !conservative_types_ref);
    optwrite = (fun b -> conservative_types_ref := b) }
@@ -608,7 +604,6 @@ let file_comment () = !file_comment_ref
 
 let () = declare_string_option
   {optdepr = false;
-   optname = "Extraction File Comment";
    optkey = ["Extraction"; "File"; "Comment"];
    optread = (fun () -> !file_comment_ref);
    optwrite = (fun s -> file_comment_ref := s) }
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 9d208e1c86..930801f6fd 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -36,7 +36,6 @@ let ground_depth=ref 3
 let ()=
   let gdopt=
     { optdepr=false;
-      optname="Firstorder Depth";
       optkey=["Firstorder";"Depth"];
       optread=(fun ()->Some !ground_depth);
       optwrite=
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index bce09d8fbd..b2ee0f9370 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -320,7 +320,6 @@ open Goptions
 let functional_induction_rewrite_dependent_proofs_sig =
   {
     optdepr = false;
-    optname = "Functional Induction Rewrite Dependent";
     optkey =  ["Functional";"Induction";"Rewrite";"Dependent"];
     optread = (fun () -> !functional_induction_rewrite_dependent_proofs);
     optwrite = (fun b -> functional_induction_rewrite_dependent_proofs := b)
@@ -332,7 +331,6 @@ let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = t
 let function_debug_sig =
   {
     optdepr = false;
-    optname = "Function debug";
     optkey =  ["Function_debug"];
     optread = (fun () -> !function_debug);
     optwrite = (fun b -> function_debug := b)
@@ -416,7 +414,6 @@ let is_strict_tcc () = !strict_tcc
 let strict_tcc_sig =
   {
     optdepr = false;
-    optname = "Raw Function Tcc";
     optkey =  ["Function_raw_tcc"];
     optread = (fun () -> !strict_tcc);
     optwrite = (fun b -> strict_tcc := b)
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 81a6651745..7ea843ca69 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -368,7 +368,6 @@ let print_info_trace = ref None
 
 let () = declare_int_option {
   optdepr = false;
-  optname = "print info trace";
   optkey = ["Info" ; "Level"];
   optread = (fun () -> !print_info_trace);
   optwrite = fun n -> print_info_trace := n;
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index fe5ebf1172..7529f9fce6 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -450,7 +450,6 @@ let () =
   let open Goptions in
   declare_bool_option
     { optdepr  = false;
-      optname  = "Ltac Profiling";
       optkey   = ["Ltac"; "Profiling"];
       optread  = get_profiling;
       optwrite = set_profiling }
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 98aa649b62..6e620b71db 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2082,7 +2082,6 @@ let () =
   let open Goptions in
   declare_bool_option
     { optdepr  = false;
-      optname  = "Ltac debug";
       optkey   = ["Ltac";"Debug"];
       optread  = (fun () -> get_debug () != Tactic_debug.DebugOff);
       optwrite = vernac_debug }
@@ -2091,7 +2090,6 @@ let () =
   let open Goptions in
   declare_bool_option
     { optdepr  = false;
-      optname  = "Ltac Backtrace";
       optkey   = ["Ltac"; "Backtrace"];
       optread  = (fun () -> !log_trace);
       optwrite = (fun b -> log_trace := b) }
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 539536911c..0e9465839a 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -86,7 +86,6 @@ open Goptions
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "Ltac batch debug";
       optkey   = ["Ltac";"Batch";"Debug"];
       optread  = (fun () -> !batch);
       optwrite = (fun x -> batch := x) }
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index ba759441e5..92110d7a43 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -68,7 +68,6 @@ open Goptions
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "unfolding of not in intuition";
       optkey   = ["Intuition";"Negation";"Unfolding"];
       optread  = (fun () -> !negation_unfolding);
       optwrite = (:=) negation_unfolding }
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index cdadde8621..4b656f8e61 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -55,7 +55,6 @@ let use_csdp_cache = ref true
 let () =
   let int_opt l vref =
     { optdepr = false
-    ; optname = List.fold_right ( ^ ) l ""
     ; optkey = l
     ; optread = (fun () -> Some !vref)
     ; optwrite =
@@ -63,42 +62,36 @@ let () =
   in
   let lia_enum_opt =
     { optdepr = false
-    ; optname = "Lia Enum"
     ; optkey = ["Lia"; "Enum"]
     ; optread = (fun () -> !lia_enum)
     ; optwrite = (fun x -> lia_enum := x) }
   in
   let solver_opt =
     { optdepr = false
-    ; optname = "Use the Simplex instead of Fourier elimination"
     ; optkey = ["Simplex"]
     ; optread = (fun () -> !Certificate.use_simplex)
     ; optwrite = (fun x -> Certificate.use_simplex := x) }
   in
   let dump_file_opt =
     { optdepr = false
-    ; optname = "Generate Coq goals in file from calls to 'lia' 'nia'"
     ; optkey = ["Dump"; "Arith"]
     ; optread = (fun () -> !Certificate.dump_file)
     ; optwrite = (fun x -> Certificate.dump_file := x) }
   in
   let lia_cache_opt =
     { optdepr = false
-    ; optname = "cache of lia (.lia.cache)"
     ; optkey = ["Lia"; "Cache"]
     ; optread = (fun () -> !use_lia_cache)
     ; optwrite = (fun x -> use_lia_cache := x) }
   in
   let nia_cache_opt =
     { optdepr = false
-    ; optname = "cache of nia (.nia.cache)"
     ; optkey = ["Nia"; "Cache"]
     ; optread = (fun () -> !use_nia_cache)
     ; optwrite = (fun x -> use_nia_cache := x) }
   in
   let nra_cache_opt =
     { optdepr = false
-    ; optname = "cache of nra (.nra.cache)"
     ; optkey = ["Nra"; "Cache"]
     ; optread = (fun () -> !use_nra_cache)
     ; optwrite = (fun x -> use_nra_cache := x) }
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 979e5bb8d8..118db01ecb 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -67,7 +67,6 @@ open Goptions
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "Omega system time displaying flag";
       optkey   = ["Omega";"System"];
       optread  = read display_system_flag;
       optwrite = write display_system_flag }
@@ -75,7 +74,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "Omega action display flag";
       optkey   = ["Omega";"Action"];
       optread  = read display_action_flag;
       optwrite = write display_action_flag }
@@ -83,7 +81,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "Omega old style flag";
       optkey   = ["Omega";"OldStyle"];
       optread  = read old_style_flag;
       optwrite = write old_style_flag }
@@ -91,7 +88,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = true;
-      optname  = "Omega automatic reset of generated names";
       optkey   = ["Stable";"Omega"];
       optread  = read reset_flag;
       optwrite = write reset_flag }
@@ -99,7 +95,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "Omega takes advantage of context variables with body";
       optkey   = ["Omega";"UseLocalDefs"];
       optread  = read letin_flag;
       optwrite = write letin_flag }
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 4cc32cfb26..ab34489de9 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -49,7 +49,6 @@ let pruning = ref true
 
 let opt_pruning=
   {optdepr=false;
-   optname="Rtauto Pruning";
    optkey=["Rtauto";"Pruning"];
    optread=(fun () -> !pruning);
    optwrite=(fun b -> pruning:=b)}
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 0c155c9d0a..b86c8d096c 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -227,7 +227,6 @@ let verbose = ref false
 
 let opt_verbose=
   {optdepr=false;
-   optname="Rtauto Verbose";
    optkey=["Rtauto";"Verbose"];
    optread=(fun () -> !verbose);
    optwrite=(fun b -> verbose:=b)}
@@ -238,7 +237,6 @@ let check = ref false
 
 let opt_check=
   {optdepr=false;
-   optname="Rtauto Check";
    optkey=["Rtauto";"Check"];
    optread=(fun () -> !check);
    optwrite=(fun b -> check:=b)}
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index cdda84a18d..df001b6084 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -34,8 +34,7 @@ open Tacmach
 let ssroldreworder = Summary.ref ~name:"SSR:oldreworder" false
 let () =
   Goptions.(declare_bool_option
-    { optname  = "ssreflect 1.3 compatibility flag";
-      optkey   = ["SsrOldRewriteGoalsOrder"];
+    { optkey   = ["SsrOldRewriteGoalsOrder"];
       optread  = (fun _ -> !ssroldreworder);
       optdepr  = false;
       optwrite = (fun b -> ssroldreworder := b) })
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index f486d1e457..235dfc257d 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -69,8 +69,7 @@ let ssrhaveNOtcresolution = Summary.ref ~name:"SSR:havenotcresolution" false
 
 let () =
   Goptions.(declare_bool_option
-    { optname  = "have type classes";
-      optkey   = ["SsrHave";"NoTCResolution"];
+    { optkey   = ["SsrHave";"NoTCResolution"];
       optread  = (fun _ -> !ssrhaveNOtcresolution);
       optdepr  = false;
       optwrite = (fun b -> ssrhaveNOtcresolution := b);
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) })
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index f0aed1a934..22250202b5 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -134,8 +134,7 @@ let ppdebug_ref = ref (fun _ -> ())
 let ssr_pp s = Feedback.msg_debug (str"SSR: "++Lazy.force s)
 let () =
   Goptions.(declare_bool_option
-    { optname  = "ssreflect debugging";
-      optkey   = ["Debug";"Ssreflect"];
+    { optkey   = ["Debug";"Ssreflect"];
       optdepr  = false;
       optread  = (fun _ -> !ppdebug_ref == ssr_pp);
       optwrite = (fun b ->
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 6cb464918a..2f6d69935a 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -55,8 +55,7 @@ let debug b =
   if b then pp_ref := ssr_pp else pp_ref := fun _ -> ()
 let _ =
   Goptions.declare_bool_option
-    { Goptions.optname  = "ssrmatching debugging";
-      Goptions.optkey   = ["Debug";"SsrMatching"];
+    { Goptions.optkey   = ["Debug";"SsrMatching"];
       Goptions.optdepr  = false;
       Goptions.optread  = (fun _ -> !pp_ref == ssr_pp);
       Goptions.optwrite = debug }
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 2b7ccbbcad..11c97221ec 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -196,7 +196,6 @@ let cofixp_reducible flgs _ stk =
 let get_debug_cbv = Goptions.declare_bool_option_and_ref
     ~depr:false
     ~value:false
-    ~name:"cbv visited constants display"
     ~key:["Debug";"Cbv"]
 
 (* Reduction of primitives *)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 3c7f9a8f00..c4aa3479bf 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -36,7 +36,6 @@ open Globnames
 let get_use_typeclasses_for_conversion =
   Goptions.declare_bool_option_and_ref
     ~depr:false
-    ~name:"use typeclass resolution during conversion"
     ~key:["Typeclass"; "Resolution"; "For"; "Conversion"]
     ~value:true
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index b042437a22..83078660c5 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -228,7 +228,6 @@ let force_wildcard () = !wildcard_value
 
 let () = declare_bool_option
           { optdepr  = false;
-            optname  = "forced wildcard";
             optkey   = ["Printing";"Wildcard"];
             optread  = force_wildcard;
             optwrite = (:=) wildcard_value }
@@ -237,7 +236,6 @@ let fast_name_generation = ref false
 
 let () = declare_bool_option {
   optdepr = false;
-  optname = "fast bound name generation algorithm";
   optkey = ["Fast";"Name";"Printing"];
   optread = (fun () -> !fast_name_generation);
   optwrite = (:=) fast_name_generation;
@@ -248,7 +246,6 @@ let synthetize_type () = !synth_type_value
 
 let () = declare_bool_option
           { optdepr  = false;
-            optname  = "pattern matching return type synthesizability";
             optkey   = ["Printing";"Synth"];
             optread  = synthetize_type;
             optwrite = (:=) synth_type_value }
@@ -258,7 +255,6 @@ let reverse_matching () = !reverse_matching_value
 
 let () = declare_bool_option
           { optdepr  = false;
-            optname  = "pattern-matching reversibility";
             optkey   = ["Printing";"Matching"];
             optread  = reverse_matching;
             optwrite = (:=) reverse_matching_value }
@@ -268,7 +264,6 @@ let print_primproj_params () = !print_primproj_params_value
 
 let () = declare_bool_option
           { optdepr  = false;
-            optname  = "printing of primitive projection parameters";
             optkey   = ["Printing";"Primitive";"Projection";"Parameters"];
             optread  = print_primproj_params;
             optwrite = (:=) print_primproj_params_value }
@@ -348,7 +343,6 @@ let print_factorize_match_patterns = ref true
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "factorization of \"match\" patterns in printing";
       optkey   = ["Printing";"Factorizable";"Match";"Patterns"];
       optread  = (fun () -> !print_factorize_match_patterns);
       optwrite = (fun b -> print_factorize_match_patterns := b) }
@@ -358,7 +352,6 @@ let print_allow_match_default_clause = ref true
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "possible use of \"match\" default pattern in printing";
       optkey   = ["Printing";"Allow";"Match";"Default";"Clause"];
       optread  = (fun () -> !print_allow_match_default_clause);
       optwrite = (fun b -> print_allow_match_default_clause := b) }
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3bd52088c7..371c528864 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -50,8 +50,6 @@ let default_flags env =
 let debug_unification = ref (false)
 let () = Goptions.(declare_bool_option {
   optdepr = false;
-  optname =
-    "Print states sent to Evarconv unification";
   optkey = ["Debug";"Unification"];
   optread = (fun () -> !debug_unification);
   optwrite = (fun a -> debug_unification:=a);
@@ -60,8 +58,6 @@ let () = Goptions.(declare_bool_option {
 let debug_ho_unification = ref (false)
 let () = Goptions.(declare_bool_option {
   optdepr = false;
-  optname =
-    "Print higher-order unification debug information";
   optkey = ["Debug";"HO";"Unification"];
   optread = (fun () -> !debug_ho_unification);
   optwrite = (fun a -> debug_ho_unification:=a);
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2d98d48aa0..ac1a4e88ef 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -125,7 +125,6 @@ let esearch_guard ?loc env sigma indexes fix =
 let is_strict_universe_declarations =
   Goptions.declare_bool_option_and_ref
     ~depr:false
-    ~name:"strict universe declaration"
     ~key:["Strict";"Universe";"Declaration"]
     ~value:true
 
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 1bc31646dd..9c478844aa 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -78,7 +78,6 @@ open Goptions
 let () =
   declare_bool_option
   { optdepr  = false;
-    optname  = "preferred transparency of Program obligations";
     optkey   = ["Transparent";"Obligations"];
     optread  = get_proofs_transparency;
     optwrite = set_proofs_transparency; }
@@ -86,7 +85,6 @@ let () =
 let () =
   declare_bool_option
   { optdepr  = false;
-    optname  = "program cases";
     optkey   = ["Program";"Cases"];
     optread  = (fun () -> !program_cases);
     optwrite = (:=) program_cases }
@@ -94,7 +92,6 @@ let () =
 let () =
   declare_bool_option
   { optdepr  = false;
-    optname  = "program generalized coercion";
     optkey   = ["Program";"Generalized";"Coercion"];
     optread  = (fun () -> !program_generalized_coercion);
     optwrite = (:=) program_generalized_coercion }
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index d5beebe690..bfee07e7f0 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -32,8 +32,6 @@ exception Elimconst
 
 let () = Goptions.(declare_bool_option {
   optdepr = false;
-  optname =
-    "Generate weak constraints between Irrelevant universes";
   optkey = ["Cumulativity";"Weak";"Constraints"];
   optread = (fun () -> not !UState.drop_weak_constraints);
   optwrite = (fun a -> UState.drop_weak_constraints:=not a);
@@ -972,8 +970,6 @@ module CredNative = RedNative(CNativeEntries)
 let debug_RAKAM = ref (false)
 let () = Goptions.(declare_bool_option {
   optdepr = false;
-  optname =
-    "Print states of the Reductionops abstract machine";
   optkey = ["Debug";"RAKAM"];
   optread = (fun () -> !debug_RAKAM);
   optwrite = (fun a -> debug_RAKAM:=a);
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 1541e96635..bcdd02b3ce 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -31,7 +31,6 @@ type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen
 let get_typeclasses_unique_solutions =
   Goptions.declare_bool_option_and_ref
     ~depr:false
-    ~name:"check that typeclasses proof search returns unique solutions"
     ~key:["Typeclasses";"Unique";"Solutions"]
     ~value:false
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 2157c4ef6a..5b87603d54 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -46,7 +46,6 @@ module NamedDecl = Context.Named.Declaration
 let keyed_unification = ref (false)
 let () = Goptions.(declare_bool_option {
   optdepr = false;
-  optname = "Unification is keyed";
   optkey = ["Keyed";"Unification"];
   optread = (fun () -> !keyed_unification);
   optwrite = (fun a -> keyed_unification:=a);
@@ -57,8 +56,6 @@ let is_keyed_unification () = !keyed_unification
 let debug_unification = ref (false)
 let () = Goptions.(declare_bool_option {
   optdepr = false;
-  optname =
-    "Print states sent to tactic unification";
   optkey = ["Debug";"Tactic";"Unification"];
   optread = (fun () -> !debug_unification);
   optwrite = (fun a -> debug_unification:=a);
diff --git a/printing/printer.ml b/printing/printer.ml
index 8af4d1d932..cc83a1dde0 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -38,7 +38,6 @@ let () =
   let open Goptions in
   declare_bool_option
     { optdepr  = false;
-      optname  = "printing of unfocused goal";
       optkey   = ["Printing";"Unfocused"];
       optread  = (fun () -> !enable_unfocused_goal_printing);
       optwrite = (fun b -> enable_unfocused_goal_printing:=b) }
@@ -49,7 +48,6 @@ let () =
   let open Goptions in
   declare_bool_option
     { optdepr  = false;
-      optname  = "printing of goal tags";
       optkey   = ["Printing";"Goal";"Tags"];
       optread  = (fun () -> !enable_goal_tags_printing);
       optwrite = (fun b -> enable_goal_tags_printing:=b) }
@@ -59,7 +57,6 @@ let () =
   let open Goptions in
   declare_bool_option
     { optdepr  = false;
-      optname  = "printing of goal names";
       optkey   = ["Printing";"Goal";"Names"];
       optread  = (fun () -> !enable_goal_names_printing);
       optwrite = (fun b -> enable_goal_names_printing:=b) }
@@ -416,7 +413,6 @@ let () =
   let open Goptions in
   declare_int_option
     { optdepr  = false;
-      optname  = "the hypotheses limit";
       optkey   = ["Hyps";"Limit"];
       optread  = (fun () -> !print_hyps_limit);
       optwrite = (fun x -> print_hyps_limit := x) }
@@ -625,7 +621,6 @@ let () =
   let open Goptions in
   declare_bool_option
     { optdepr  = false;
-      optname  = "Printing Dependent Evars Line";
       optkey   = ["Printing";"Dependent";"Evars";"Line"];
       optread  = (fun () -> !should_print_dependent_evars);
       optwrite = (fun v -> should_print_dependent_evars := v) }
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 85bb287c22..a5fd7f69ed 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -44,7 +44,6 @@ let short = ref false
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "short module printing";
       optkey   = ["Short";"Module";"Printing"];
       optread  = (fun () -> !short) ;
       optwrite = ((:=) short) }
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index dec87f8071..d93dd15f91 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -69,7 +69,6 @@ let write_diffs_option opt =
 let () =
   Goptions.(declare_string_option {
     optdepr = false;
-    optname = "show diffs in proofs";
     optkey = ["Diffs"];
     optread = read_diffs_option;
     optwrite = write_diffs_option
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
diff --git a/stm/stm.ml b/stm/stm.ml
index 4c539684e3..5402600041 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2849,7 +2849,6 @@ let process_back_meta_command ~newtip ~head oid aast =
 let get_allow_nested_proofs =
   Goptions.declare_bool_option_and_ref
     ~depr:false
-    ~name:"Nested Proofs Allowed"
     ~key:Vernac_classifier.stm_allow_nested_proofs_option_name
     ~value:false
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 9c1a975330..1dde820075 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -177,7 +177,6 @@ let global_info_auto = ref false
 let add_option ls refe =
   Goptions.(declare_bool_option
     { optdepr  = false;
-      optname  = String.concat " " ls;
       optkey   = ls;
       optread  = (fun () -> !refe);
       optwrite = (:=) refe })
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index ccd88d2c35..28feeecb86 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -83,8 +83,6 @@ open Goptions
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "do typeclass search avoiding eta-expansions " ^
-                   " in proof terms (expensive)";
       optkey   = ["Typeclasses";"Limit";"Intros"];
       optread  = get_typeclasses_limit_intros;
       optwrite = set_typeclasses_limit_intros; }
@@ -92,7 +90,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "during typeclass resolution, solve instances according to their dependency order";
       optkey   = ["Typeclasses";"Dependency";"Order"];
       optread  = get_typeclasses_dependency_order;
       optwrite = set_typeclasses_dependency_order; }
@@ -100,7 +97,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "use iterative deepening strategy";
       optkey   = ["Typeclasses";"Iterative";"Deepening"];
       optread  = get_typeclasses_iterative_deepening;
       optwrite = set_typeclasses_iterative_deepening; }
@@ -108,7 +104,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "compat";
       optkey   = ["Typeclasses";"Filtered";"Unification"];
       optread  = get_typeclasses_filtered_unification;
       optwrite = set_typeclasses_filtered_unification; }
@@ -116,7 +111,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "debug output for typeclasses proof search";
       optkey   = ["Typeclasses";"Debug"];
       optread  = get_typeclasses_debug;
       optwrite = set_typeclasses_debug; }
@@ -124,7 +118,6 @@ let () =
 let _ =
   declare_int_option
     { optdepr  = false;
-      optname  = "verbosity of debug output for typeclasses proof search";
       optkey   = ["Typeclasses";"Debug";"Verbosity"];
       optread  = get_typeclasses_verbose;
       optwrite = set_typeclasses_verbose; }
@@ -132,7 +125,6 @@ let _ =
 let () =
   declare_int_option
     { optdepr  = false;
-      optname  = "depth for typeclasses proof search";
       optkey   = ["Typeclasses";"Depth"];
       optread  = get_typeclasses_depth;
       optwrite = set_typeclasses_depth; }
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 80ca124912..9a1e6a6736 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -331,7 +331,6 @@ let global_info_eauto = ref false
 let () =
   Goptions.(declare_bool_option
     { optdepr  = false;
-      optname  = "Debug Eauto";
       optkey   = ["Debug";"Eauto"];
       optread  = (fun () -> !global_debug_eauto);
       optwrite = (:=) global_debug_eauto })
@@ -339,7 +338,6 @@ let () =
 let () =
   Goptions.(declare_bool_option
     { optdepr  = false;
-      optname  = "Info Eauto";
       optkey   = ["Info";"Eauto"];
       optread  = (fun () -> !global_info_eauto);
       optwrite = (:=) global_info_eauto })
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 9195746dc6..146483b846 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -72,7 +72,6 @@ let use_injection_in_context = function
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "injection in context";
       optkey   = ["Structural";"Injection"];
       optread  = (fun () -> !injection_in_context) ;
       optwrite = (fun b -> injection_in_context := b) }
@@ -734,7 +733,6 @@ let keep_proof_equalities_for_injection = ref false
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "injection on prop arguments";
       optkey   = ["Keep";"Proof";"Equalities"];
       optread  = (fun () -> !keep_proof_equalities_for_injection) ;
       optwrite = (fun b -> keep_proof_equalities_for_injection := b) }
@@ -1686,7 +1684,6 @@ let regular_subst_tactic = ref true
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "more regular behavior of tactic subst";
       optkey   = ["Regular";"Subst";"Tactic"];
       optread  = (fun () -> !regular_subst_tactic);
       optwrite = (:=) regular_subst_tactic }
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 73e8331bcb..86aa046586 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -205,7 +205,6 @@ let write_warn_hint = function
 let () =
   Goptions.(declare_string_option
     { optdepr  = false;
-      optname  = "behavior of non-imported hints";
       optkey   = ["Loose"; "Hint"; "Behavior"];
       optread  = read_warn_hint;
       optwrite = write_warn_hint;
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index a4a06873b8..72204e1d24 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -17,7 +17,6 @@ open Evd
 let use_unification_heuristics_ref = ref true
 let () = Goptions.(declare_bool_option {
   optdepr = false;
-  optname = "Solve unification constraints at every \".\"";
   optkey = ["Solve";"Unification";"Constraints"];
   optread = (fun () -> !use_unification_heuristics_ref);
   optwrite = (fun a -> use_unification_heuristics_ref:=a);
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index b1fd34e43c..4c470519d6 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -143,7 +143,6 @@ let private_poly_univs =
   let b = ref true in
   let _ = Goptions.(declare_bool_option {
       optdepr = false;
-      optname = "use private polymorphic universes for Qed constants";
       optkey = ["Private";"Polymorphic";"Universes"];
       optread = (fun () -> !b);
       optwrite = ((:=) b);
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index fc7b126ee5..a30c877435 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -56,8 +56,6 @@ let strong_cbn flags =
 let simplIsCbn = ref (false)
 let () = Goptions.(declare_bool_option {
   optdepr = false;
-  optname =
-    "Plug the simpl tactic to the new cbn mechanism";
   optkey = ["SimplIsCbn"];
   optread = (fun () -> !simplIsCbn);
   optwrite = (fun a -> simplIsCbn:=a);
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 609b752716..18fe200606 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -67,7 +67,6 @@ let use_clear_hyp_by_default () = !clear_hyp_by_default
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "default clearing of hypotheses after use";
       optkey   = ["Default";"Clearing";"Used";"Hypotheses"];
       optread  = (fun () -> !clear_hyp_by_default) ;
       optwrite = (fun b -> clear_hyp_by_default := b) }
@@ -83,7 +82,6 @@ let accept_universal_lemma_under_conjunctions () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "trivial unification in tactics applying under conjunctions";
       optkey   = ["Universal";"Lemma";"Under";"Conjunction"];
       optread  = (fun () -> !universal_lemma_under_conjunctions) ;
       optwrite = (fun b -> universal_lemma_under_conjunctions := b) }
@@ -102,7 +100,6 @@ let use_bracketing_last_or_and_intro_pattern () =
 let () =
   declare_bool_option
     { optdepr  = true;
-      optname  = "bracketing last or-and introduction pattern";
       optkey   = ["Bracketing";"Last";"Introduction";"Pattern"];
       optread  = (fun () -> !bracketing_last_or_and_intro_pattern);
       optwrite = (fun b -> bracketing_last_or_and_intro_pattern := b) }
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 977cae6254..7e3baac7d6 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -368,7 +368,7 @@ let top_goal_print ~doc c oldp newp =
 
 let exit_on_error =
   let open Goptions in
-  declare_bool_option_and_ref ~depr:false ~name:"coqtop-exit-on-error" ~key:["Coqtop";"Exit";"On";"Error"]
+  declare_bool_option_and_ref ~depr:false ~key:["Coqtop";"Exit";"On";"Error"]
     ~value:false
 
 let rec vernac_loop ~state =
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index bcc5f54505..d6db4a735c 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -824,7 +824,6 @@ let register_struct ?local str = match str with
 
 let _ = Goptions.declare_bool_option {
   Goptions.optdepr = false;
-  Goptions.optname = "print Ltac2 backtrace";
   Goptions.optkey = ["Ltac2"; "Backtrace"];
   Goptions.optread = (fun () -> !Tac2interp.print_ltac2_backtrace);
   Goptions.optwrite = (fun b -> Tac2interp.print_ltac2_backtrace := b);
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 68d2c3a00d..194308b77f 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -154,7 +154,6 @@ let program_mode = ref false
 let () = let open Goptions in
   declare_bool_option
     { optdepr  = false;
-      optname  = "use of the program extension";
       optkey   = program_mode_option_name;
       optread  = (fun () -> !program_mode);
       optwrite = (fun b -> program_mode:=b) }
@@ -188,7 +187,6 @@ let is_universe_polymorphism =
   let () = let open Goptions in
     declare_bool_option
       { optdepr  = false;
-        optname  = "universe polymorphism";
         optkey   = universe_polymorphism_option_name;
         optread  = (fun () -> !b);
         optwrite = ((:=) b) }
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index dce0a70f72..d711c9aea0 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -42,7 +42,6 @@ let should_auto_template =
   let auto = ref true in
   let () = declare_bool_option
       { optdepr  = false;
-        optname  = "Automatically make some inductive types template polymorphic";
         optkey   = ["Auto";"Template";"Polymorphism"];
         optread  = (fun () -> !auto);
         optwrite = (fun b -> auto := b); }
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index b56b9c8ce2..dcb28b898f 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -56,7 +56,7 @@ type program_info =
 
 let get_shrink_obligations =
   Goptions.declare_bool_option_and_ref ~depr:true (* remove in 8.8 *)
-    ~name:"Shrinking of Program obligations" ~key:["Shrink"; "Obligations"]
+    ~key:["Shrink"; "Obligations"]
     ~value:true
 
 (* XXX: Is this the right place for this? *)
@@ -133,7 +133,6 @@ let add_hint local prg cst =
 let get_hide_obligations =
   Goptions.declare_bool_option_and_ref
     ~depr:false
-    ~name:"Hidding of Program obligations"
     ~key:["Hide"; "Obligations"]
     ~value:false
 
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 2f0b1062a7..227d2f1554 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -44,7 +44,6 @@ let elim_flag = ref true
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "automatic declaration of induction schemes";
       optkey   = ["Elimination";"Schemes"];
       optread  = (fun () -> !elim_flag) ;
       optwrite = (fun b -> elim_flag := b) }
@@ -53,7 +52,6 @@ let bifinite_elim_flag = ref false
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "automatic declaration of induction schemes for non-recursive types";
       optkey   = ["Nonrecursive";"Elimination";"Schemes"];
       optread  = (fun () -> !bifinite_elim_flag) ;
       optwrite = (fun b -> bifinite_elim_flag := b) }
@@ -62,7 +60,6 @@ let case_flag = ref false
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "automatic declaration of case analysis schemes";
       optkey   = ["Case";"Analysis";"Schemes"];
       optread  = (fun () -> !case_flag) ;
       optwrite = (fun b -> case_flag := b) }
@@ -71,7 +68,6 @@ let eq_flag = ref false
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "automatic declaration of boolean equality";
       optkey   = ["Boolean";"Equality";"Schemes"];
       optread  = (fun () -> !eq_flag) ;
       optwrite = (fun b -> eq_flag := b) }
@@ -82,7 +78,6 @@ let eq_dec_flag = ref false
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "automatic declaration of decidable equality";
       optkey   = ["Decidable";"Equality";"Schemes"];
       optread  = (fun () -> !eq_dec_flag) ;
       optwrite = (fun b -> eq_dec_flag := b) }
@@ -91,7 +86,6 @@ let rewriting_flag = ref false
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  ="automatic declaration of rewriting schemes for equality types";
       optkey   = ["Rewriting";"Schemes"];
       optread  = (fun () -> !rewriting_flag) ;
       optwrite = (fun b -> rewriting_flag := b) }
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 865eded545..f7606f4ede 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -268,7 +268,6 @@ let warn_let_as_axiom =
 let get_keep_admitted_vars =
   Goptions.declare_bool_option_and_ref
     ~depr:false
-    ~name:"keep section variables in admitted proofs"
     ~key:["Keep"; "Admitted"; "Variables"]
     ~value:true
 
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index cfb3248c7b..b329463cb0 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -140,7 +140,6 @@ let suggest_proof_using = ref false
 let () =
   Goptions.(declare_bool_option
     { optdepr  = false;
-      optname  = "suggest Proof using";
       optkey   = ["Suggest";"Proof";"Using"];
       optread  = (fun () -> !suggest_proof_using);
       optwrite = ((:=) suggest_proof_using) })
@@ -176,7 +175,6 @@ let proof_using_opt_name = ["Default";"Proof";"Using"]
 let () =
   Goptions.(declare_stringopt_option
     { optdepr  = false;
-      optname  = "default value for Proof using";
       optkey   = proof_using_opt_name;
       optread  = (fun () -> Option.map using_to_string !value);
       optwrite = (fun b -> value := Option.map using_from_string b);
diff --git a/vernac/record.ml b/vernac/record.ml
index f6945838d7..27bd390714 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -39,7 +39,6 @@ let primitive_flag = ref false
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "use of primitive projections";
       optkey   = ["Primitive";"Projections"];
       optread  = (fun () -> !primitive_flag) ;
       optwrite = (fun b -> primitive_flag := b) }
@@ -48,7 +47,6 @@ let typeclasses_strict = ref false
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "strict typeclass resolution";
       optkey   = ["Typeclasses";"Strict";"Resolution"];
       optread  = (fun () -> !typeclasses_strict);
       optwrite = (fun b -> typeclasses_strict := b); }
@@ -57,7 +55,6 @@ let typeclasses_unique = ref false
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "unique typeclass instances";
       optkey   = ["Typeclasses";"Unique";"Instances"];
       optread  = (fun () -> !typeclasses_unique);
       optwrite = (fun b -> typeclasses_unique := b); }
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index fd588f5b15..f8eef68997 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -611,7 +611,6 @@ let vernac_assumption ~atts discharge kind l nl =
 
 let is_polymorphic_inductive_cumulativity =
   declare_bool_option_and_ref ~depr:false ~value:false
-    ~name:"Polymorphic inductive cumulativity"
     ~key:["Polymorphic"; "Inductive"; "Cumulativity"]
 
 let should_treat_as_cumulative cum poly =
@@ -627,7 +626,6 @@ let should_treat_as_cumulative cum poly =
 let get_uniform_inductive_parameters =
   Goptions.declare_bool_option_and_ref
     ~depr:false
-    ~name:"Uniform inductive parameters"
     ~key:["Uniform"; "Inductive"; "Parameters"]
     ~value:false
 
@@ -1220,7 +1218,6 @@ let vernac_generalizable ~local =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "allow sprop";
       optkey   = ["Allow";"StrictProp"];
       optread  = (fun () -> Global.sprop_allowed());
       optwrite = Global.set_allow_sprop }
@@ -1228,7 +1225,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "silent";
       optkey   = ["Silent"];
       optread  = (fun () -> !Flags.quiet);
       optwrite = ((:=) Flags.quiet) }
@@ -1236,7 +1232,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "implicit arguments";
       optkey   = ["Implicit";"Arguments"];
       optread  = Impargs.is_implicit_args;
       optwrite = Impargs.make_implicit_args }
@@ -1244,7 +1239,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "strict implicit arguments";
       optkey   = ["Strict";"Implicit"];
       optread  = Impargs.is_strict_implicit_args;
       optwrite = Impargs.make_strict_implicit_args }
@@ -1252,7 +1246,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "strong strict implicit arguments";
       optkey   = ["Strongly";"Strict";"Implicit"];
       optread  = Impargs.is_strongly_strict_implicit_args;
       optwrite = Impargs.make_strongly_strict_implicit_args }
@@ -1260,7 +1253,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "contextual implicit arguments";
       optkey   = ["Contextual";"Implicit"];
       optread  = Impargs.is_contextual_implicit_args;
       optwrite = Impargs.make_contextual_implicit_args }
@@ -1268,7 +1260,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "implicit status of reversible patterns";
       optkey   = ["Reversible";"Pattern";"Implicit"];
       optread  = Impargs.is_reversible_pattern_implicit_args;
       optwrite = Impargs.make_reversible_pattern_implicit_args }
@@ -1276,7 +1267,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "maximal insertion of implicit";
       optkey   = ["Maximal";"Implicit";"Insertion"];
       optread  = Impargs.is_maximal_implicit_args;
       optwrite = Impargs.make_maximal_implicit_args }
@@ -1284,7 +1274,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "coercion printing";
       optkey   = ["Printing";"Coercions"];
       optread  = (fun () -> !Constrextern.print_coercions);
       optwrite = (fun b ->  Constrextern.print_coercions := b) }
@@ -1292,7 +1281,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "printing of existential variable instances";
       optkey   = ["Printing";"Existential";"Instances"];
       optread  = (fun () -> !Detyping.print_evar_arguments);
       optwrite = (:=) Detyping.print_evar_arguments }
@@ -1300,7 +1288,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "implicit arguments printing";
       optkey   = ["Printing";"Implicit"];
       optread  = (fun () -> !Constrextern.print_implicits);
       optwrite = (fun b ->  Constrextern.print_implicits := b) }
@@ -1308,7 +1295,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "implicit arguments defensive printing";
       optkey   = ["Printing";"Implicit";"Defensive"];
       optread  = (fun () -> !Constrextern.print_implicits_defensive);
       optwrite = (fun b ->  Constrextern.print_implicits_defensive := b) }
@@ -1316,7 +1302,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "projection printing using dot notation";
       optkey   = ["Printing";"Projections"];
       optread  = (fun () -> !Constrextern.print_projections);
       optwrite = (fun b ->  Constrextern.print_projections := b) }
@@ -1324,7 +1309,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "notations printing";
       optkey   = ["Printing";"Notations"];
       optread  = (fun () -> not !Constrextern.print_no_symbol);
       optwrite = (fun b ->  Constrextern.print_no_symbol := not b) }
@@ -1332,7 +1316,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "raw printing";
       optkey   = ["Printing";"All"];
       optread  = (fun () -> !Flags.raw_print);
       optwrite = (fun b -> Flags.raw_print := b) }
@@ -1340,7 +1323,6 @@ let () =
 let () =
   declare_int_option
     { optdepr  = false;
-      optname  = "the level of inlining during functor application";
       optkey   = ["Inline";"Level"];
       optread  = (fun () -> Some (Flags.get_inline_level ()));
       optwrite = (fun o ->
@@ -1350,7 +1332,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "kernel term sharing";
       optkey   = ["Kernel"; "Term"; "Sharing"];
       optread  = (fun () -> (Global.typing_flags ()).Declarations.share_reduction);
       optwrite = Global.set_share_reduction }
@@ -1358,7 +1339,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "display compact goal contexts";
       optkey   = ["Printing";"Compact";"Contexts"];
       optread  = (fun () -> Printer.get_compact_context());
       optwrite = (fun b -> Printer.set_compact_context b) }
@@ -1366,7 +1346,6 @@ let () =
 let () =
   declare_int_option
     { optdepr  = false;
-      optname  = "the printing depth";
       optkey   = ["Printing";"Depth"];
       optread  = Topfmt.get_depth_boxes;
       optwrite = Topfmt.set_depth_boxes }
@@ -1374,7 +1353,6 @@ let () =
 let () =
   declare_int_option
     { optdepr  = false;
-      optname  = "the printing width";
       optkey   = ["Printing";"Width"];
       optread  = Topfmt.get_margin;
       optwrite = Topfmt.set_margin }
@@ -1382,7 +1360,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "printing of universes";
       optkey   = ["Printing";"Universes"];
       optread  = (fun () -> !Constrextern.print_universes);
       optwrite = (fun b -> Constrextern.print_universes:=b) }
@@ -1390,7 +1367,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "dumping bytecode after compilation";
       optkey   = ["Dump";"Bytecode"];
       optread  = (fun () -> !Cbytegen.dump_bytecode);
       optwrite = (:=) Cbytegen.dump_bytecode }
@@ -1398,7 +1374,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "dumping VM lambda code after compilation";
       optkey   = ["Dump";"Lambda"];
       optread  = (fun () -> !Clambda.dump_lambda);
       optwrite = (:=) Clambda.dump_lambda }
@@ -1406,7 +1381,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "explicitly parsing implicit arguments";
       optkey   = ["Parsing";"Explicit"];
       optread  = (fun () -> !Constrintern.parsing_explicit);
       optwrite = (fun b ->  Constrintern.parsing_explicit := b) }
@@ -1414,7 +1388,6 @@ let () =
 let () =
   declare_string_option ~preprocess:CWarnings.normalize_flags_string
     { optdepr  = false;
-      optname  = "warnings display";
       optkey   = ["Warnings"];
       optread  = CWarnings.get_flags;
       optwrite = CWarnings.set_flags }
@@ -1422,7 +1395,6 @@ let () =
 let () =
   declare_string_option
     { optdepr  = false;
-      optname  = "native_compute profiler output";
       optkey   = ["NativeCompute"; "Profile"; "Filename"];
       optread  = Nativenorm.get_profile_filename;
       optwrite = Nativenorm.set_profile_filename }
@@ -1430,7 +1402,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "enable native compute profiling";
       optkey   = ["NativeCompute"; "Profiling"];
       optread  = Nativenorm.get_profiling_enabled;
       optwrite = Nativenorm.set_profiling_enabled }
@@ -1438,7 +1409,6 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "enable native compute timing";
       optkey   = ["NativeCompute"; "Timing"];
       optread  = Nativenorm.get_timing_enabled;
       optwrite = Nativenorm.set_timing_enabled }
@@ -1446,7 +1416,6 @@ let () =
 let _ =
   declare_bool_option
     { optdepr  = false;
-      optname  = "guard checking";
       optkey   = ["Guard"; "Checking"];
       optread  = (fun () -> (Global.typing_flags ()).Declarations.check_guarded);
       optwrite = (fun b -> Global.set_check_guarded b) }
@@ -1454,7 +1423,6 @@ let _ =
 let _ =
   declare_bool_option
     { optdepr  = false;
-      optname  = "positivity/productivity checking";
       optkey   = ["Positivity"; "Checking"];
       optread  = (fun () -> (Global.typing_flags ()).Declarations.check_positive);
       optwrite = (fun b -> Global.set_check_positive b) }
@@ -1462,7 +1430,6 @@ let _ =
 let _ =
   declare_bool_option
     { optdepr  = false;
-      optname  = "universes checking";
       optkey   = ["Universe"; "Checking"];
       optread  = (fun () -> (Global.typing_flags ()).Declarations.check_universes);
       optwrite = (fun b -> Global.set_check_universes b) }
@@ -1777,7 +1744,6 @@ let search_output_name_only = ref false
 let () =
   declare_bool_option
     { optdepr  = false;
-      optname  = "output-name-only search";
       optkey   = ["Search";"Output";"Name";"Only"];
       optread  = (fun () -> !search_output_name_only);
       optwrite = (:=) search_output_name_only }
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index c14fc78462..1ec09b6beb 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -65,7 +65,6 @@ let proof_mode_opt_name = ["Default";"Proof";"Mode"]
 let () =
   Goptions.declare_string_option Goptions.{
     optdepr = false;
-    optname = "default proof mode" ;
     optkey = proof_mode_opt_name;
     optread = get_default_proof_mode_opt;
     optwrite = set_default_proof_mode_opt;
@@ -249,7 +248,6 @@ let interp_qed_delayed_control ~proof ~info ~st ~control { CAst.loc; v=pe } =
 let () = let open Goptions in
   declare_int_option
     { optdepr  = false;
-      optname  = "the default timeout";
       optkey   = ["Default";"Timeout"];
       optread  = (fun () -> !default_timeout);
       optwrite = ((:=) default_timeout) }