From 80dfe0cb64285f58dfe2eebd7319c747c70d3d6b Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 7 Apr 2017 09:49:21 +0200 Subject: Add a version to be used when parsing compatibility notations mentioning old versions. --- toplevel/coqinit.ml | 3 ++- toplevel/coqinit.mli | 2 +- toplevel/coqtop.ml | 4 +++- 3 files changed, 6 insertions(+), 3 deletions(-) (limited to 'toplevel') diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 16fe40555..33b032704 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -126,7 +126,7 @@ let init_ocaml_path () = Mltop.add_ml_dir (Envars.coqlib ()); List.iter add_subdir Coq_config.all_src_dirs -let get_compat_version = function +let get_compat_version ?(allow_old = true) = function | "8.7" -> Flags.Current | "8.6" -> Flags.V8_6 | "8.5" -> Flags.V8_5 @@ -134,6 +134,7 @@ let get_compat_version = function | "8.3" -> Flags.V8_3 | "8.2" -> Flags.V8_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.") | s -> CErrors.user_err ~hdr:"get_compat_version" diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 3b42289ee..787dfb61a 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -25,4 +25,4 @@ val init_library_roots : unit -> unit val init_ocaml_path : unit -> unit -val get_compat_version : string -> Flags.compat_version +val get_compat_version : ?allow_old:bool -> string -> Flags.compat_version diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 31450ebd5..7a487f809 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -514,7 +514,9 @@ let parse_args arglist = |"-async-proofs-delegation-threshold" -> Flags.async_proofs_delegation_threshold:= get_float opt (next ()) |"-worker-id" -> set_worker_id opt (next ()) - |"-compat" -> let v = get_compat_version (next ()) in Flags.compat_version := v; add_compat_require v + |"-compat" -> + let v = get_compat_version ~allow_old:false (next ()) in + Flags.compat_version := v; add_compat_require v |"-compile" -> add_compile false (next ()) |"-compile-verbose" -> add_compile true (next ()) |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true -- cgit v1.2.3 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(-) (limited to 'toplevel') 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 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. --- lib/flags.ml | 6 +----- lib/flags.mli | 2 +- pretyping/unification.ml | 8 ++------ tactics/equality.ml | 2 +- toplevel/coqinit.ml | 3 +-- 5 files changed, 6 insertions(+), 15 deletions(-) (limited to 'toplevel') diff --git a/lib/flags.ml b/lib/flags.ml index c4a97bd12..d738e3df1 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_3 | V8_4 | V8_5 | V8_6 | Current +type compat_version = VOld | 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_3, V8_3 -> 0 - | V8_3, _ -> -1 - | _, V8_3 -> 1 | V8_4, V8_4 -> 0 | V8_4, _ -> -1 | _, V8_4 -> 1 @@ -133,7 +130,6 @@ let version_less_or_equal v = not (version_strictly_greater v) let pr_version = function | VOld -> "old" - | V8_3 -> "8.3" | V8_4 -> "8.4" | V8_5 -> "8.5" | V8_6 -> "8.6" diff --git a/lib/flags.mli b/lib/flags.mli index 6e9362681..d6a0eac44 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_3 | V8_4 | V8_5 | V8_6 | Current +type compat_version = VOld | 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/pretyping/unification.ml b/pretyping/unification.ml index 3e0eb9d91..ef4f7f754 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -484,8 +484,7 @@ let use_evars_pattern_unification flags = let use_metas_pattern_unification sigma flags nb l = !global_pattern_unification_flag && flags.use_pattern_unification - || (Flags.version_less_or_equal Flags.V8_3 || - flags.use_meta_bound_pattern_unification) && + || flags.use_meta_bound_pattern_unification && Array.for_all (fun c -> isRel sigma c && destRel sigma c <= nb) l type key = @@ -608,9 +607,6 @@ let do_reduce ts (env, nb) sigma c = Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma Cst_stack.empty (c, Stack.empty))) -let use_full_betaiota flags = - flags.modulo_betaiota && Flags.version_strictly_greater Flags.V8_3 - let isAllowedEvar sigma flags c = match EConstr.kind sigma c with | Evar (evk,_) -> not (Evar.Set.mem evk flags.frozen_evars) | _ -> false @@ -948,7 +944,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e expand curenvnb pb opt substn cM f1 l1 cN f2 l2 and reduce curenvnb pb opt (sigma, metas, evars as substn) cM cN = - if use_full_betaiota flags && not (subterm_restriction opt flags) then + if flags.modulo_betaiota && not (subterm_restriction opt flags) then let cM' = do_reduce flags.modulo_delta curenvnb sigma cM in if not (EConstr.eq_constr sigma cM cM') then unirec_rec curenvnb pb opt substn cM' cN diff --git a/tactics/equality.ml b/tactics/equality.ml index 46c042b8b..5c2370253 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 diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index af0c18fa2..4a17a5ee1 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -131,8 +131,7 @@ let get_compat_version ?(allow_old = true) = function | "8.6" -> Flags.V8_6 | "8.5" -> Flags.V8_5 | "8.4" -> Flags.V8_4 - | "8.3" -> Flags.V8_3 - | ("8.2" | "8.1" | "8.0") as s -> + | ("8.3" | "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.") -- 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. --- doc/stdlib/index-list.html.template | 1 - engine/namegen.ml | 3 +- lib/flags.ml | 6 +-- lib/flags.mli | 2 +- tactics/equality.ml | 4 +- tactics/tactics.ml | 1 - test-suite/bugs/closed/4394.v | 19 --------- test-suite/bugs/closed/4400.v | 19 --------- test-suite/bugs/closed/4656.v | 4 -- test-suite/bugs/closed/4727.v | 10 ----- test-suite/bugs/closed/4733.v | 52 ------------------------ test-suite/bugs/opened/4803.v | 48 ---------------------- test-suite/success/Compat84.v | 19 --------- theories/Compat/Coq84.v | 79 ------------------------------------- toplevel/coqinit.ml | 3 +- toplevel/coqtop.ml | 1 - 16 files changed, 5 insertions(+), 266 deletions(-) delete mode 100644 test-suite/bugs/closed/4394.v delete mode 100644 test-suite/bugs/closed/4400.v delete mode 100644 test-suite/bugs/closed/4656.v delete mode 100644 test-suite/bugs/closed/4727.v delete mode 100644 test-suite/bugs/closed/4733.v delete mode 100644 test-suite/bugs/opened/4803.v delete mode 100644 test-suite/success/Compat84.v delete mode 100644 theories/Compat/Coq84.v (limited to 'toplevel') diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 1b847414f..48f82f2d9 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -589,7 +589,6 @@ through the Require Import command.

theories/Compat/AdmitAxiom.v - theories/Compat/Coq84.v theories/Compat/Coq85.v theories/Compat/Coq86.v
diff --git a/engine/namegen.ml b/engine/namegen.ml index 5bd62273c..e635dc163 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -412,8 +412,7 @@ let rename_bound_vars_as_displayed sigma avoid env c = let h_based_elimination_names = ref false -let use_h_based_elimination_names () = - !h_based_elimination_names && Flags.version_strictly_greater Flags.V8_4 +let use_h_based_elimination_names () = !h_based_elimination_names open Goptions diff --git a/lib/flags.ml b/lib/flags.ml index d738e3df1..13539bced 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_4 | V8_5 | V8_6 | Current +type compat_version = VOld | 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_4, V8_4 -> 0 - | V8_4, _ -> -1 - | _, V8_4 -> 1 | V8_5, V8_5 -> 0 | V8_5, _ -> -1 | _, V8_5 -> 1 @@ -130,7 +127,6 @@ let version_less_or_equal v = not (version_strictly_greater v) let pr_version = function | VOld -> "old" - | V8_4 -> "8.4" | V8_5 -> "8.5" | V8_6 -> "8.6" | Current -> "current" diff --git a/lib/flags.mli b/lib/flags.mli index d6a0eac44..0026aba2e 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_4 | V8_5 | V8_6 | Current +type compat_version = VOld | 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/tactics/equality.ml b/tactics/equality.ml index 5c2370253..d7ec52762 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 ebfaab5bf..96e7be763 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 diff --git a/test-suite/bugs/closed/4394.v b/test-suite/bugs/closed/4394.v deleted file mode 100644 index 1ad81345d..000000000 --- a/test-suite/bugs/closed/4394.v +++ /dev/null @@ -1,19 +0,0 @@ -(* -*- coq-prog-args: ("-compat" "8.4") -*- *) - -Require Import Equality List. -Inductive Foo (I : Type -> Type) (A : Type) : Type := -| foo (B : Type) : A -> I B -> Foo I A. -Definition Family := Type -> Type. -Definition FooToo : Family -> Family := Foo. -Definition optionize (I : Type -> Type) (A : Type) := option (I A). -Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo (optionize I) A := foo (optionize I) A A. -Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }. -Definition barRec : Rec (optionize id) := {| rec := bar id |}. -Inductive Empty {T} : T -> Prop := . -Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family) nil)) (b : unit) : - Empty (a, b) -> False. -Proof. - intro e. - dependent induction e. -Qed. - diff --git a/test-suite/bugs/closed/4400.v b/test-suite/bugs/closed/4400.v deleted file mode 100644 index a89cf0cbc..000000000 --- a/test-suite/bugs/closed/4400.v +++ /dev/null @@ -1,19 +0,0 @@ -(* -*- coq-prog-args: ("-require" "Coq.Compat.Coq84" "-compat" "8.4") -*- *) -Require Import Coq.Lists.List Coq.Logic.JMeq Program.Equality. -Set Printing Universes. -Inductive Foo (I : Type -> Type) (A : Type) : Type := -| foo (B : Type) : A -> I B -> Foo I A. -Definition Family := Type -> Type. -Definition FooToo : Family -> Family := Foo. -Definition optionize (I : Type -> Type) (A : Type) := option (I A). -Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo(optionize I) A := foo (optionize I) A A. -Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }. -Definition barRec : Rec (optionize id) := {| rec := bar id |}. -Inductive Empty {T} : T -> Prop := . -Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family) -nil)) (b : unit) : - Empty (a, b) -> False. -Proof. - intro e. - dependent induction e. -Qed. diff --git a/test-suite/bugs/closed/4656.v b/test-suite/bugs/closed/4656.v deleted file mode 100644 index a59eed2c8..000000000 --- a/test-suite/bugs/closed/4656.v +++ /dev/null @@ -1,4 +0,0 @@ -(* -*- coq-prog-args: ("-compat" "8.4") -*- *) -Goal True. - constructor 1. -Qed. diff --git a/test-suite/bugs/closed/4727.v b/test-suite/bugs/closed/4727.v deleted file mode 100644 index cfb4548d2..000000000 --- a/test-suite/bugs/closed/4727.v +++ /dev/null @@ -1,10 +0,0 @@ -(* -*- coq-prog-args: ("-compat" "8.4") -*- *) -Goal forall (P : Set) (l : P) (P0 : Set) (w w0 : P0) (T : Type) (a : P * T) (o : P -> option P0), - (forall (l1 l2 : P) (w1 : P0), o l1 = Some w1 -> o l2 = Some w1 -> l1 = l2) -> - o l = Some w -> o (fst a) = Some w0 -> {w = w0} + {w <> w0} -> False. -Proof. - clear; intros ???????? inj H0 H1 H2. - destruct H2; intuition subst. - eapply inj in H1; [ | eauto ]. - progress subst. (* should succeed, used to not succeed *) -Abort. diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v deleted file mode 100644 index a90abd71c..000000000 --- a/test-suite/bugs/closed/4733.v +++ /dev/null @@ -1,52 +0,0 @@ -(* -*- coq-prog-args: ("-compat" "8.4") -*- *) -(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5. If they use*) -Require Import Coq.Lists.List. -Require Import Coq.Vectors.Vector. -Import ListNotations. -Import VectorNotations. -Set Implicit Arguments. -Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T). -Arguments mynil {_}, _. - -Delimit Scope mylist_scope with mylist. -Bind Scope mylist_scope with mylist. -Delimit Scope vector_scope with vector. - -Notation " [ ] " := mynil (format "[ ]") : mylist_scope. -Notation " [ x ] " := (mycons x mynil) : mylist_scope. -Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope. - -(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4. There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *) -Check [ ]%mylist : mylist _. -Check [ ]%list : list _. -Check []%vector : Vector.t _ _. -Check [ _ ]%mylist : mylist _. -Check [ _ ]%list : list _. -Check [ _ ]%vector : Vector.t _ _. -Check [ _ ; _ ]%list : list _. -Check [ _ ; _ ]%vector : Vector.t _ _. -Check [ _ ; _ ]%mylist : mylist _. -Check [ _ ; _ ; _ ]%list : list _. -Check [ _ ; _ ; _ ]%vector : Vector.t _ _. -Check [ _ ; _ ; _ ]%mylist : mylist _. -Check [ _ ; _ ; _ ; _ ]%list : list _. -Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. -Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. - -Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope. -(* Now these all work, but not so in 8.4. If we get the ability to remove notations, this section can also just be removed. *) -Check [ ]%mylist : mylist _. -Check [ ]%list : list _. -Check []%vector : Vector.t _ _. -Check [ _ ]%mylist : mylist _. -Check [ _ ]%list : list _. -Check [ _ ]%vector : Vector.t _ _. -Check [ _ ; _ ]%list : list _. -Check [ _ ; _ ]%vector : Vector.t _ _. -Check [ _ ; _ ]%mylist : mylist _. -Check [ _ ; _ ; _ ]%list : list _. -Check [ _ ; _ ; _ ]%vector : Vector.t _ _. -Check [ _ ; _ ; _ ]%mylist : mylist _. -Check [ _ ; _ ; _ ; _ ]%list : list _. -Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. -Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v deleted file mode 100644 index 4541f13d0..000000000 --- a/test-suite/bugs/opened/4803.v +++ /dev/null @@ -1,48 +0,0 @@ -(* -*- coq-prog-args: ("-compat" "8.4") -*- *) -(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5. If they use*) -Require Import Coq.Lists.List. -Require Import Coq.Vectors.Vector. -Import ListNotations. -Import VectorNotations. -Set Implicit Arguments. -Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T). -Arguments mynil {_}, _. - -Delimit Scope mylist_scope with mylist. -Bind Scope mylist_scope with mylist. -Delimit Scope vector_scope with vector. - -Notation " [ ] " := mynil (format "[ ]") : mylist_scope. -Notation " [ x ] " := (mycons x mynil) : mylist_scope. -Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope. - -(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4. There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *) -Check [ ]%mylist : mylist _. -Check [ ]%list : list _. -Check []%vector : Vector.t _ _. -Check [ _ ]%mylist : mylist _. -Check [ _ ]%list : list _. -Check [ _ ]%vector : Vector.t _ _. -Check [ _ ; _ ]%list : list _. -Check [ _ ; _ ]%vector : Vector.t _ _. -Check [ _ ; _ ]%mylist : mylist _. -Check [ _ ; _ ; _ ]%list : list _. -Check [ _ ; _ ; _ ]%vector : Vector.t _ _. -Check [ _ ; _ ; _ ]%mylist : mylist _. -Check [ _ ; _ ; _ ; _ ]%list : list _. -Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. -Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. - -(** Now check that we can add and then remove notations from the parser *) -(* We should be able to stick some vernacular here to remove [] from the parser *) -Fail Remove Notation "[]". -Goal True. - (* This should not be a syntax error; before moving this file to closed, uncomment this line. *) - (* idtac; []. *) - constructor. -Qed. - -Check { _ : _ & _ }. -Reserved Infix "&" (at level 0). -Fail Remove Infix "&". -(* Check { _ : _ & _ }. *) diff --git a/test-suite/success/Compat84.v b/test-suite/success/Compat84.v deleted file mode 100644 index 732a024fc..000000000 --- a/test-suite/success/Compat84.v +++ /dev/null @@ -1,19 +0,0 @@ -(* -*- coq-prog-args: ("-compat" "8.4") -*- *) - -Goal True. - solve [ constructor 1 ]. Undo. - solve [ econstructor 1 ]. Undo. - solve [ constructor ]. Undo. - solve [ econstructor ]. Undo. - solve [ constructor (fail) ]. Undo. - solve [ econstructor (fail) ]. Undo. - split. -Qed. - -Goal False \/ True. - solve [ constructor (constructor) ]. Undo. - solve [ econstructor (econstructor) ]. Undo. - solve [ constructor 2; constructor ]. Undo. - solve [ econstructor 2; econstructor ]. Undo. - right; esplit. -Qed. diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v deleted file mode 100644 index a3e23f91c..000000000 --- a/theories/Compat/Coq84.v +++ /dev/null @@ -1,79 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* -> sig. -Coercion sigT_of_sigT2 : sigT2 >-> sigT. -Coercion sigT_of_sig : sig >-> sigT. -Coercion sig_of_sigT : sigT >-> sig. -Coercion sigT2_of_sig2 : sig2 >-> sigT2. -Coercion sig2_of_sigT2 : sigT2 >-> sig2. - -(** In 8.4, the statement of admitted lemmas did not depend on the section - variables. *) -Unset Keep Admitted Variables. diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 4a17a5ee1..f36d0c348 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -130,8 +130,7 @@ let get_compat_version ?(allow_old = true) = function | "8.7" -> Flags.Current | "8.6" -> Flags.V8_6 | "8.5" -> Flags.V8_5 - | "8.4" -> Flags.V8_4 - | ("8.3" | "8.2" | "8.1" | "8.0") as s -> + | ("8.4" | "8.3" | "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/toplevel/coqtop.ml b/toplevel/coqtop.ml index 7a487f809..3e4365605 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -205,7 +205,6 @@ let require () = let add_compat_require v = match v with - | Flags.V8_4 -> add_require "Coq.Compat.Coq84" | Flags.V8_5 -> add_require "Coq.Compat.Coq85" | _ -> () -- cgit v1.2.3 From 165e3000844c1e84cc5c9d1b579a0a7dab8a3684 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 7 Apr 2017 10:05:12 +0200 Subject: Add support for Coq 8.6. --- toplevel/coqtop.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'toplevel') diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 3e4365605..5f0716fd9 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -206,7 +206,8 @@ let require () = let add_compat_require v = match v with | Flags.V8_5 -> add_require "Coq.Compat.Coq85" - | _ -> () + | Flags.V8_6 -> add_require "Coq.Compat.Coq86" + | Flags.VOld | Flags.Current -> () let compile_list = ref ([] : (bool * string) list) -- cgit v1.2.3