diff options
| author | ppedrot | 2011-11-24 14:18:19 +0000 |
|---|---|---|
| committer | ppedrot | 2011-11-24 14:18:19 +0000 |
| commit | fabae66b541378df3ff0c1e941b38759c19f6129 (patch) | |
| tree | efb605b835ce2d58378b2a15a4211698da3b017a /tactics | |
| parent | 1f26b8591f3698699ee2143f5244a5d57243e283 (diff) | |
Added a DEPRECATED flag in declaration of options. For now only two options are declared as such, but I suspect Coq to contain some more.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14724 85f007b7-540e-0410-9357-904b9bb8a0f7
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); |