Merge PR #11521: Remove Goptions.opt_name field

Reviewed-by: Zimmi48
Reviewed-by: ppedrot

9 files changed, 0 insertions, 22 deletions

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 9ef5f478d3..7393454ba9 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 2d900a237a..8371da76b2 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) }