Merge PR #11521: Remove Goptions.opt_name field

Reviewed-by: Zimmi48
Reviewed-by: ppedrot

9 files changed, 0 insertions, 25 deletions

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 c21af82659..c67019c7ac 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 d5c8c3bd19..aa2e96c2d7 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);