Merge PR #11521: Remove Goptions.opt_name field

Reviewed-by: Zimmi48
Reviewed-by: ppedrot

18 files changed, 6 insertions, 43 deletions

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 915531cf3c..e45bae19ca 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -54,8 +54,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 }