diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 1 | ||||
| -rw-r--r-- | tactics/tactics.ml | 1 | ||||
| -rw-r--r-- | tactics/tauto.ml4 | 1 |
4 files changed, 5 insertions, 0 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index c332993975..82b4267759 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -694,6 +694,7 @@ let get_typeclasses_debug () = !typeclasses_debug let set_typeclasses_debug = declare_bool_option { optsync = true; + optdepr = false; optname = "debug output for typeclasses proof search"; optkey = ["Typeclasses";"Debug"]; optread = get_typeclasses_debug; @@ -708,6 +709,7 @@ let get_typeclasses_depth () = !typeclasses_depth let set_typeclasses_depth = declare_int_option { optsync = true; + optdepr = false; optname = "depth for typeclasses proof search"; optkey = ["Typeclasses";"Depth"]; optread = get_typeclasses_depth; diff --git a/tactics/equality.ml b/tactics/equality.ml index b037ea7e2a..76bceb738f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -56,6 +56,7 @@ open Goptions let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "automatic introduction of hypotheses by discriminate"; optkey = ["Discriminate";"Introduction"]; optread = (fun () -> !discriminate_introduction); diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cddb7a2b29..25a148bbdb 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -72,6 +72,7 @@ let use_dependent_propositions_elimination () = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "dependent-propositions-elimination tactic"; optkey = ["Dependent";"Propositions";"Elimination"]; optread = (fun () -> !dependent_propositions_elimination) ; diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 46f8c9bb4b..b7a58be455 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -53,6 +53,7 @@ open Goptions let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "unfolding of iff and not in intuition"; optkey = ["Intuition";"Iff";"Unfolding"]; optread = (fun () -> !iff_unfolding); |