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.

9 files changed, 1 insertions, 53 deletions

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) }