From 0e06c54a9249477fdab5b135ffdac4bd3ea501a5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 24 Jan 2015 21:27:54 +0100
Subject: 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).

---
 tactics/tactics.ml | 15 ---------------
 1 file changed, 15 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f1f1248d7c..07969c7d74 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
-- 
cgit v1.2.3