Remove support for Coq 8.4.

16 files changed, 5 insertions, 266 deletions

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 <tt>Require Import</tt> command.</p>
   </dt>
   <dd>
     theories/Compat/AdmitAxiom.v
-    theories/Compat/Coq84.v
     theories/Compat/Coq85.v
     theories/Compat/Coq86.v
   </dd>
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     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Compatibility file for making Coq act similar to Coq v8.4 *)
-
-(** Any compatibility changes to make future versions of Coq behave like Coq 8.5 are likely needed to make them behave like Coq 8.4. *)
-Require Export Coq.Compat.Coq85.
-
-(** See https://coq.inria.fr/bugs/show_bug.cgi?id=4319 for updates *)
-(** This is required in Coq 8.5 to use the [omega] tactic; in Coq 8.4, it's automatically available.  But ZArith_base puts infix ~ at level 7, and we don't want that, so we don't [Import] it. *)
-Require Coq.omega.Omega.
-Ltac omega := Coq.omega.Omega.omega.
-
-(** The number of arguments given in [match] statements has changed from 8.4 to 8.5. *)
-Global Set Asymmetric Patterns.
-
-(** The automatic elimination schemes for records were dropped by default in 8.5.  This restores the default behavior of Coq 8.4. *)
-Global Set Nonrecursive Elimination Schemes.
-
-(** See bug 3545 *)
-Global Set Universal Lemma Under Conjunction.
-
-(** Feature introduced in 8.5, disabled by default and configurable since 8.6. *)
-Global Unset Refolding Reduction.
-
-(** In 8.4, [constructor (tac)] allowed backtracking across the use of [constructor]; it has been subsumed by [constructor; tac]. *)
-Ltac constructor_84_n n := constructor n.
-Ltac constructor_84_tac tac := once (constructor; tac).
-
-Tactic Notation "constructor" := Coq.Init.Notations.constructor.
-Tactic Notation "constructor" int_or_var(n) := constructor_84_n n.
-Tactic Notation "constructor" "(" tactic(tac) ")" := constructor_84_tac tac.
-
-(** In 8.4, [econstructor (tac)] allowed backtracking across the use of [econstructor]; it has been subsumed by [econstructor; tac]. *)
-Ltac econstructor_84_n n := econstructor n.
-Ltac econstructor_84_tac tac := once (econstructor; tac).
-
-Tactic Notation "econstructor" := Coq.Init.Notations.econstructor.
-Tactic Notation "econstructor" int_or_var(n) := econstructor_84_n n.
-Tactic Notation "econstructor" "(" tactic(tac) ")" := econstructor_84_tac tac.
-
-(** Some tactic notations do not factor well with tactics; we add global parsing entries for some tactics that would otherwise be overwritten by custom variants. See https://coq.inria.fr/bugs/show_bug.cgi?id=4392. *)
-Tactic Notation "reflexivity" := reflexivity.
-Tactic Notation "assumption" := assumption.
-Tactic Notation "etransitivity" := etransitivity.
-Tactic Notation "cut" constr(c) := cut c.
-Tactic Notation "exact_no_check" constr(c) := exact_no_check c.
-Tactic Notation "vm_cast_no_check" constr(c) := vm_cast_no_check c.
-Tactic Notation "casetype" constr(c) := casetype c.
-Tactic Notation "elimtype" constr(c) := elimtype c.
-Tactic Notation "lapply" constr(c) := lapply c.
-Tactic Notation "transitivity" constr(c) := transitivity c.
-Tactic Notation "left" := left.
-Tactic Notation "eleft" := eleft.
-Tactic Notation "right" := right.
-Tactic Notation "eright" := eright.
-Tactic Notation "symmetry" := symmetry.
-Tactic Notation "split" := split.
-Tactic Notation "esplit" := esplit.
-
-(** Many things now import [PeanoNat] rather than [NPeano], so we require it so that the old absolute names in [NPeano.Nat] are available. *)
-Require Coq.Numbers.Natural.Peano.NPeano.
-
-(** The following coercions were declared by default in Specif.v. *)
-Coercion sig_of_sig2 : sig2 >-> 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"
   | _ -> ()