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 diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 1b847414f2..48f82f2d92 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 5bd62273c8..e635dc163a 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 d738e3df18..13539bced3 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 d6a0eac444..0026aba2e3 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 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 diff --git a/test-suite/bugs/closed/4394.v b/test-suite/bugs/closed/4394.v deleted file mode 100644 index 1ad81345db..0000000000 --- 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 a89cf0cbc3..0000000000 --- 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 a59eed2c86..0000000000 --- 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 cfb4548d2c..0000000000 --- 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 a90abd71cf..0000000000 --- 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 4541f13d01..0000000000 --- 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 732a024fc1..0000000000 --- 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 a3e23f91c9..0000000000 --- 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 4a17a5ee14..f36d0c348e 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 7a487f809e..3e43656056 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