diff options
| author | Gaëtan Gilbert | 2020-02-04 17:07:34 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-12 16:23:49 +0100 |
| commit | 4563779bf990cf22d88474a68acf4eb9cfd8d173 (patch) | |
| tree | c5333864070ccc9b8746799e9236ba90ef1a432d /tactics/class_tactics.ml | |
| parent | 6c1de3455d5cd79958a8e26ac728f7d5d1b8d025 (diff) | |
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.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 8 |
1 files changed, 0 insertions, 8 deletions
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; } |