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. --- interp/constrintern.ml | 2 +- lib/flags.ml | 8 ++------ lib/flags.mli | 2 +- plugins/ltac/tauto.ml | 2 +- pretyping/classops.ml | 8 ++------ pretyping/unification.ml | 1 - tactics/equality.ml | 13 ++++--------- tactics/tactics.ml | 1 - toplevel/coqinit.ml | 3 +-- vernac/indschemes.ml | 2 +- 10 files changed, 13 insertions(+), 29 deletions(-) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 3d484a02d..67fee6202 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -786,7 +786,7 @@ let find_appl_head_data c = let scopes = find_arguments_scope ref in c, impls, scopes, [] | GApp ({ v = GRef (ref,_) },l) - when l != [] && Flags.version_strictly_greater Flags.V8_2 -> + when l != [] -> let n = List.length l in let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in diff --git a/lib/flags.ml b/lib/flags.ml index 682e2e4df..c4a97bd12 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -106,7 +106,7 @@ let we_are_parsing = ref false (* Current means no particular compatibility consideration. For correct comparisons, this constructor should remain the last one. *) -type compat_version = VOld | V8_2 | V8_3 | V8_4 | V8_5 | V8_6 | Current +type compat_version = VOld | V8_3 | V8_4 | V8_5 | V8_6 | Current let compat_version = ref Current @@ -114,9 +114,6 @@ let version_compare v1 v2 = match v1, v2 with | VOld, VOld -> 0 | VOld, _ -> -1 | _, VOld -> 1 - | V8_2, V8_2 -> 0 - | V8_2, _ -> -1 - | _, V8_2 -> 1 | V8_3, V8_3 -> 0 | V8_3, _ -> -1 | _, V8_3 -> 1 @@ -136,7 +133,6 @@ let version_less_or_equal v = not (version_strictly_greater v) let pr_version = function | VOld -> "old" - | V8_2 -> "8.2" | V8_3 -> "8.3" | V8_4 -> "8.4" | V8_5 -> "8.5" @@ -161,7 +157,7 @@ let is_verbose () = not !quiet let auto_intros = ref true let make_auto_intros flag = auto_intros := flag -let is_auto_intros () = version_strictly_greater V8_2 && !auto_intros +let is_auto_intros () = !auto_intros let universe_polymorphism = ref false let make_universe_polymorphism b = universe_polymorphism := b diff --git a/lib/flags.mli b/lib/flags.mli index c0aca9c99..6e9362681 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -77,7 +77,7 @@ val raw_print : bool ref (* Univ print flag, never set anywere. Maybe should belong to Univ? *) val univ_print : bool ref -type compat_version = VOld | V8_2 | V8_3 | V8_4 | V8_5 | V8_6 | Current +type compat_version = VOld | V8_3 | V8_4 | V8_5 | V8_6 | Current val compat_version : compat_version ref val version_compare : compat_version -> compat_version -> int val version_strictly_greater : compat_version -> bool diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 5eacb1a95..c6cc955b0 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -66,7 +66,7 @@ let negation_unfolding = ref true (* Whether inner iff are unfolded *) let iff_unfolding = ref false -let unfold_iff () = !iff_unfolding || Flags.version_less_or_equal Flags.V8_2 +let unfold_iff () = !iff_unfolding open Goptions let _ = diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 9a973cff5..627a9c9cc 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -454,15 +454,11 @@ let cache_coercion (_, c) = add_coercion_in_graph (xf,is,it) let load_coercion _ o = - if - !automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2 - then + if !automatically_import_coercions then cache_coercion o let open_coercion i o = - if Int.equal i 1 && not - (!automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2) - then + if Int.equal i 1 && not !automatically_import_coercions then cache_coercion o let subst_coercion (subst, c) = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 0fb48ed8c..3e0eb9d91 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -481,7 +481,6 @@ let set_flags_for_type flags = { flags with let use_evars_pattern_unification flags = !global_pattern_unification_flag && flags.use_pattern_unification - && Flags.version_strictly_greater Flags.V8_2 let use_metas_pattern_unification sigma flags nb l = !global_pattern_unification_flag && flags.use_pattern_unification diff --git a/tactics/equality.ml b/tactics/equality.ml index 05c5cd5ec..46c042b8b 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 b553f316c..ebfaab5bf 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 diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 33b032704..af0c18fa2 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -132,8 +132,7 @@ let get_compat_version ?(allow_old = true) = function | "8.5" -> Flags.V8_5 | "8.4" -> Flags.V8_4 | "8.3" -> Flags.V8_3 - | "8.2" -> Flags.V8_2 - | ("8.1" | "8.0") as s -> + | ("8.2" | "8.1" | "8.0") as s -> if allow_old then Flags.VOld else CErrors.user_err ~hdr:"get_compat_version" (str "Compatibility with version " ++ str s ++ str " not supported.") diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index c2c27eb78..e90c25926 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -92,7 +92,7 @@ let _ = (* compatibility *) optread = (fun () -> !eq_flag) ; optwrite = (fun b -> eq_flag := b) } -let is_eq_flag () = !eq_flag && Flags.version_strictly_greater Flags.V8_2 +let is_eq_flag () = !eq_flag let eq_dec_flag = ref false let _ = -- cgit v1.2.3