From 571c319ed536cb2757176d3ae4007a75f5d3b04d Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Nov 2016 17:08:14 +0100 Subject: Remove support for Coq 8.2. --- tactics/equality.ml | 13 ++++--------- tactics/tactics.ml | 1 - 2 files changed, 4 insertions(+), 10 deletions(-) (limited to 'tactics') diff --git a/tactics/equality.ml b/tactics/equality.ml index 05c5cd5ec1..46c042b8be 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -50,8 +50,7 @@ module NamedDecl = Context.Named.Declaration let discriminate_introduction = ref true -let discr_do_intro () = - !discriminate_introduction && Flags.version_strictly_greater Flags.V8_2 +let discr_do_intro () = !discriminate_introduction open Goptions let _ = @@ -356,7 +355,6 @@ let find_elim hdcncl lft2rgt dep cls ot gl = if (is_global Coqlib.glob_eq hdcncl || (is_global Coqlib.glob_jmeq hdcncl && jmeq_same_dom gl ot)) && not dep - || Flags.version_less_or_equal Flags.V8_2 then let c = match EConstr.kind sigma hdcncl with @@ -1769,13 +1767,10 @@ type subst_tactic_flags = { rewrite_dependent_proof : bool } -let default_subst_tactic_flags () = - if Flags.version_strictly_greater Flags.V8_2 then - { only_leibniz = false; rewrite_dependent_proof = true } - else - { only_leibniz = true; rewrite_dependent_proof = false } +let default_subst_tactic_flags = + { only_leibniz = false; rewrite_dependent_proof = true } -let subst_all ?(flags=default_subst_tactic_flags ()) () = +let subst_all ?(flags=default_subst_tactic_flags) () = if !regular_subst_tactic then diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b553f316c2..ebfaab5bfe 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -64,7 +64,6 @@ let dependent_propositions_elimination = ref true let use_dependent_propositions_elimination () = !dependent_propositions_elimination - && Flags.version_strictly_greater Flags.V8_2 let _ = declare_bool_option -- cgit v1.2.3 From daf5335b18c926d7130cd28e50f00cc49c4011f6 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Nov 2016 17:12:58 +0100 Subject: Remove support for Coq 8.3. --- tactics/equality.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/equality.ml b/tactics/equality.ml index 46c042b8be..5c23702536 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1416,7 +1416,7 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause = "" else " You can try to use option Set Keep Proof Equalities." in tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion)) - | Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 -> + | Inr [([],_,_)] -> tclZEROMSG (str"Nothing to inject.") | Inr posns -> inject_at_positions env sigma l2r u eq_clause posns -- cgit v1.2.3 From bcaf9af83363f3e1a1c588271e5038984ee1760b Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 8 Apr 2017 07:04:56 +0200 Subject: Remove support for Coq 8.4. --- tactics/equality.ml | 4 +--- tactics/tactics.ml | 1 - 2 files changed, 1 insertion(+), 4 deletions(-) (limited to 'tactics') diff --git a/tactics/equality.ml b/tactics/equality.ml index 5c23702536..d7ec527629 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -63,9 +63,7 @@ let _ = let injection_pattern_l2r_order = ref true -let use_injection_pattern_l2r_order () = - !injection_pattern_l2r_order - && Flags.version_strictly_greater Flags.V8_4 +let use_injection_pattern_l2r_order () = !injection_pattern_l2r_order let _ = declare_bool_option diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ebfaab5bfe..96e7be763d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -141,7 +141,6 @@ let bracketing_last_or_and_intro_pattern = ref true let use_bracketing_last_or_and_intro_pattern () = !bracketing_last_or_and_intro_pattern - && Flags.version_strictly_greater Flags.V8_4 let _ = declare_bool_option -- cgit v1.2.3 From 5e93f1e95853c3614df813845b94051a45f1a749 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Nov 2016 17:51:32 +0100 Subject: Deprecate options that were introduced for compatibility with 8.2. --- tactics/equality.ml | 2 +- tactics/tactics.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'tactics') diff --git a/tactics/equality.ml b/tactics/equality.ml index d7ec527629..d810e862af 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -55,7 +55,7 @@ let discr_do_intro () = !discriminate_introduction open Goptions let _ = declare_bool_option - { optdepr = false; + { optdepr = true; (* remove in 8.8 *) 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 96e7be763d..dbb613c40e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -67,7 +67,7 @@ let use_dependent_propositions_elimination () = let _ = declare_bool_option - { optdepr = false; + { optdepr = true; (* remove in 8.8 *) optname = "dependent-propositions-elimination tactic"; optkey = ["Dependent";"Propositions";"Elimination"]; optread = (fun () -> !dependent_propositions_elimination) ; -- cgit v1.2.3 From 180b3739bb6601ff9aaf951e4b87e0bb45341b77 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Nov 2016 17:54:14 +0100 Subject: Deprecate options that were introduced for compatibility with 8.4. --- tactics/equality.ml | 2 +- tactics/tactics.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'tactics') diff --git a/tactics/equality.ml b/tactics/equality.ml index d810e862af..6e56dc48e5 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -67,7 +67,7 @@ let use_injection_pattern_l2r_order () = !injection_pattern_l2r_order let _ = declare_bool_option - { optdepr = false; + { optdepr = true; (* remove in 8.8 *) optname = "injection left-to-right pattern order and clear by default when with introduction pattern"; optkey = ["Injection";"L2R";"Pattern";"Order"]; optread = (fun () -> !injection_pattern_l2r_order) ; diff --git a/tactics/tactics.ml b/tactics/tactics.ml index dbb613c40e..f56a913cbe 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -144,7 +144,7 @@ let use_bracketing_last_or_and_intro_pattern () = let _ = declare_bool_option - { optdepr = false; + { optdepr = true; (* remove in 8.8 *) optname = "bracketing last or-and introduction pattern"; optkey = ["Bracketing";"Last";"Introduction";"Pattern"]; optread = (fun () -> !bracketing_last_or_and_intro_pattern); -- cgit v1.2.3