diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-24 21:27:54 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-24 22:27:57 +0100 |
| commit | 0e06c54a9249477fdab5b135ffdac4bd3ea501a5 (patch) | |
| tree | 71d5cc86ab1d09f6fed685319a734d45661b839f | |
| parent | 14787df2ea09994151e886bf918aca0aecbd8ade (diff) | |
Removed obsolete option "Legacy Partially Applied Elimination
Argument" which I used temporarily in a branch to have "destruct eq_dec"
working like in v8.4 and not like the "destruct (eq_dec _ _)"
of 8.4. I finally made "destruct (eq_dec _ _)" working in 8.5 like
"destruct eq_dec" was working in 8.4 (and is still working in 8.5).
| -rw-r--r-- | tactics/tactics.ml | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f1f1248d7..07969c7d7 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -59,22 +59,7 @@ let dloc = Loc.ghost let typ_of = Retyping.get_type_of -(* Option for 8.4 compatibility *) open Goptions -let legacy_elim_if_not_fully_applied_argument = ref false - -let use_legacy_elim_if_not_fully_applied_argument () = - !legacy_elim_if_not_fully_applied_argument - || Flags.version_less_or_equal Flags.V8_4 - -let _ = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "partially applied elimination argument legacy"; - optkey = ["Legacy";"Partially";"Applied";"Elimination";"Argument"]; - optread = (fun () -> !legacy_elim_if_not_fully_applied_argument) ; - optwrite = (fun b -> legacy_elim_if_not_fully_applied_argument := b) } (* Option for 8.2 compatibility *) let dependent_propositions_elimination = ref true |