Merge PR #8638: Remove -compat 8.7

Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: jfehrle
Ack-by: maximedenes
Reviewed-by: ppedrot

32 files changed, 16 insertions, 274 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 08893655b0..6f54060d34 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -84,6 +84,14 @@ Notations
   constant `Nat.gcd` in the parameter-argument of `eq_refl`).  See
   #9840 for more details.
 
+- Deprecated compatibility notations have actually been removed.  Uses
+  of these notations are generally easy to fix thanks to the hint
+  contained in the deprecation warnings. For projects that require
+  more than a handful of such fixes, there is [a
+  script](https://gist.github.com/JasonGross/9770653967de3679d131c59d42de6d17#file-replace-notations-py)
+  that will do it automatically, using the output of coqc. The script
+  contains documentation on its usage in a comment at the top.
+
 Plugins
 
 - The quote plugin (https://coq.inria.fr/distrib/V8.8.1/refman/proof-engine/detailed-tactic-examples.html#quote)
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index fd79996bb7..a561de1d0c 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -619,7 +619,6 @@ through the <tt>Require Import</tt> command.</p>
   </dt>
   <dd>
     theories/Compat/AdmitAxiom.v
-    theories/Compat/Coq87.v
     theories/Compat/Coq88.v
     theories/Compat/Coq89.v
     theories/Compat/Coq810.v
diff --git a/lib/flags.ml b/lib/flags.ml
index 6718e7a954..452433d271 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -62,14 +62,11 @@ 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 = V8_7 | V8_8 | V8_9 | Current
+type compat_version = V8_8 | V8_9 | Current
 
 let compat_version = ref Current
 
 let version_compare v1 v2 = match v1, v2 with
-  | V8_7, V8_7 -> 0
-  | V8_7, _ -> -1
-  | _, V8_7 -> 1
   | V8_8, V8_8 -> 0
   | V8_8, _ -> -1
   | _, V8_8 -> 1
@@ -82,7 +79,6 @@ let version_strictly_greater v = version_compare !compat_version v > 0
 let version_less_or_equal v = not (version_strictly_greater v)
 
 let pr_version = function
-  | V8_7 -> "8.7"
   | V8_8 -> "8.8"
   | V8_9 -> "8.9"
   | Current -> "current"
diff --git a/lib/flags.mli b/lib/flags.mli
index bf8846417b..a70a23b902 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -52,7 +52,7 @@ val we_are_parsing : bool ref
 (* Set Printing All flag. For some reason it is a global flag *)
 val raw_print : bool ref
 
-type compat_version = V8_7 | V8_8 | V8_9 | Current
+type compat_version = V8_8 | V8_9 | 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/test-suite/bugs/closed/bug_4798.v b/test-suite/bugs/closed/bug_4798.v
index 696812dee1..f238086633 100644
--- a/test-suite/bugs/closed/bug_4798.v
+++ b/test-suite/bugs/closed/bug_4798.v
@@ -1,5 +1,5 @@
 (* DO NOT MODIFY THIS FILE DIRECTLY *)
 (* It is autogenerated by dev/tools/update-compat.py. *)
 Check match 2 with 0 => 0 | S n => n end.
-Notation "|" := 1 (compat "8.7").
+Notation "|" := 1 (compat "8.8").
 Check match 2 with 0 => 0 | S n => n end. (* fails *)
diff --git a/test-suite/bugs/closed/bug_9166.v b/test-suite/bugs/closed/bug_9166.v
index a89837dd12..21cd770cbb 100644
--- a/test-suite/bugs/closed/bug_9166.v
+++ b/test-suite/bugs/closed/bug_9166.v
@@ -2,7 +2,7 @@
 (* It is autogenerated by dev/tools/update-compat.py. *)
 Set Warnings "+deprecated".
 
-Notation bar := option (compat "8.7").
+Notation bar := option (compat "8.8").
 
 Definition foo (x: nat) : nat :=
   match x with
diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v
deleted file mode 100644
index 1f62635f50..0000000000
--- a/test-suite/success/CompatOldOldFlag.v
+++ /dev/null
@@ -1,6 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.7") -*- *)
-(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *)
-Import Coq.Compat.Coq810.
-Import Coq.Compat.Coq89.
-Import Coq.Compat.Coq88.
-Import Coq.Compat.Coq87.
diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh
index 61273c4f37..7ff5571ffb 100755
--- a/test-suite/tools/update-compat/run.sh
+++ b/test-suite/tools/update-compat/run.sh
@@ -6,4 +6,4 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )"
 # we assume that the script lives in test-suite/tools/update-compat/,
 # and that update-compat.py lives in dev/tools/
 cd "${SCRIPT_DIR}/../../.."
-dev/tools/update-compat.py --assert-unchanged --master || exit $?
+dev/tools/update-compat.py --assert-unchanged --release || exit $?
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 0c68b75124..e91f589d67 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -147,10 +147,6 @@ Register not_gt as num.nat.not_gt.
     See now [Nat.compare] and its properties.
     In scope [nat_scope], the notation for [Nat.compare] is "?=" *)
 
-Notation nat_compare := Nat.compare (compat "8.7").
-
-Notation nat_compare_spec := Nat.compare_spec (compat "8.7").
-Notation nat_compare_eq_iff := Nat.compare_eq_iff (compat "8.7").
 Notation nat_compare_S := Nat.compare_succ (only parsing).
 
 Lemma nat_compare_lt n m : n<m <-> (n ?= m) = Lt.
diff --git a/theories/Compat/Coq87.v b/theories/Compat/Coq87.v
deleted file mode 100644
index 5e031efa85..0000000000
--- a/theories/Compat/Coq87.v
+++ /dev/null
@@ -1,25 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Compatibility file for making Coq act similar to Coq v8.7 *)
-Local Set Warnings "-deprecated".
-
-Require Export Coq.Compat.Coq88.
-
-(* In 8.7, omega wasn't taking advantage of local abbreviations,
-   see bug 148 and PR#768. For adjusting this flag, we're forced to
-   first dynlink the omega plugin, but we should avoid doing a full
-   "Require Omega", since it has some undesired effects (at least on hints)
-   and breaks at least fiat-crypto. *)
-Declare ML Module "omega_plugin".
-Unset Omega UseLocalDefs.
-
-
-Set Typeclasses Axioms Are Instances.
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index d19c5558d8..e68bc5930d 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -26,8 +26,6 @@ Hint Extern 1 (Equivalence _) => constructor; congruence : core.
 
 Module WFacts_fun (E:DecidableType)(Import M:WSfun E).
 
-Notation option_map := option_map (compat "8.7").
-
 Notation eq_dec := E.eq_dec.
 Definition eqb x y := if eq_dec x y then true else false.
 
@@ -676,7 +674,7 @@ Qed.
 Add Parametric Morphism elt : (@Empty elt)
  with signature Equal ==> iff as Empty_m.
 Proof.
-unfold Empty; intros m m' Hm. split; intros; intro. 
+unfold Empty; intros m m' Hm. split; intros; intro.
 rewrite <-Hm in H0; eapply H, H0.
 rewrite Hm in H0; eapply H, H0.
 Qed.
@@ -758,7 +756,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
 
   Instance eqk_equiv : Equivalence eqk.
   Proof. unfold eq_key; split; eauto. Qed.
-  
+
   Instance eqke_equiv : Equivalence eqke.
   Proof.
    unfold eq_key_elt; split; repeat red; firstorder.
@@ -2198,4 +2196,3 @@ Module OrdProperties (M:S).
  End Elt.
 
 End OrdProperties.
-
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index e5d63c547d..fcec2f2fd6 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -801,19 +801,3 @@ Defined.
 
 Hint Resolve left right inleft inright: core.
 Hint Resolve exist exist2 existT existT2: core.
-
-(* Compatibility *)
-
-Notation sigS := sigT (compat "8.7").
-Notation existS := existT (compat "8.7").
-Notation sigS_rect := sigT_rect (compat "8.7").
-Notation sigS_rec := sigT_rec (compat "8.7").
-Notation sigS_ind := sigT_ind (compat "8.7").
-Notation projS1 := projT1 (compat "8.7").
-Notation projS2 := projT2 (compat "8.7").
-
-Notation sigS2 := sigT2 (compat "8.7").
-Notation existS2 := existT2 (compat "8.7").
-Notation sigS2_rect := sigT2_rect (compat "8.7").
-Notation sigS2_rec := sigT2_rec (compat "8.7").
-Notation sigS2_ind := sigT2_ind (compat "8.7").
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index b930388d13..e2ec41ca94 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -125,8 +125,6 @@ Proof.
   apply eq_dep_intro.
 Qed.
 
-Notation eq_sigS_eq_dep := eq_sigT_eq_dep (compat "8.7"). (* Compatibility *)
-
 Lemma eq_dep_eq_sigT :
   forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
     eq_dep p x q y -> existT P p x = existT P q y.
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index d319ed1029..b8da5a2ed1 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -985,33 +985,13 @@ Notation N_ind := N_ind (only parsing).
 Notation N0 := N0 (only parsing).
 Notation Npos := N.pos (only parsing).
 
-Notation Ndiscr := N.discr (compat "8.7").
 Notation Ndouble_plus_one := N.succ_double (only parsing).
-Notation Ndouble := N.double (compat "8.7").
-Notation Nsucc := N.succ (compat "8.7").
-Notation Npred := N.pred (compat "8.7").
-Notation Nsucc_pos := N.succ_pos (compat "8.7").
-Notation Ppred_N := Pos.pred_N (compat "8.7").
 Notation Nplus := N.add (only parsing).
 Notation Nminus := N.sub (only parsing).
 Notation Nmult := N.mul (only parsing).
-Notation Neqb := N.eqb (compat "8.7").
-Notation Ncompare := N.compare (compat "8.7").
-Notation Nlt := N.lt (compat "8.7").
-Notation Ngt := N.gt (compat "8.7").
-Notation Nle := N.le (compat "8.7").
-Notation Nge := N.ge (compat "8.7").
-Notation Nmin := N.min (compat "8.7").
-Notation Nmax := N.max (compat "8.7").
-Notation Ndiv2 := N.div2 (compat "8.7").
-Notation Neven := N.even (compat "8.7").
-Notation Nodd := N.odd (compat "8.7").
-Notation Npow := N.pow (compat "8.7").
-Notation Nlog2 := N.log2 (compat "8.7").
 
 Notation nat_of_N := N.to_nat (only parsing).
 Notation N_of_nat := N.of_nat (only parsing).
-Notation N_eq_dec := N.eq_dec (compat "8.7").
 Notation Nrect := N.peano_rect (only parsing).
 Notation Nrect_base := N.peano_rect_base (only parsing).
 Notation Nrect_step := N.peano_rect_succ (only parsing).
@@ -1020,11 +1000,8 @@ Notation Nrec := N.peano_rec (only parsing).
 Notation Nrec_base := N.peano_rec_base (only parsing).
 Notation Nrec_succ := N.peano_rec_succ (only parsing).
 
-Notation Npred_succ := N.pred_succ (compat "8.7").
 Notation Npred_minus := N.pred_sub (only parsing).
-Notation Nsucc_pred := N.succ_pred (compat "8.7").
 Notation Ppred_N_spec := N.pos_pred_spec (only parsing).
-Notation Nsucc_pos_spec := N.succ_pos_spec (compat "8.7").
 Notation Ppred_Nsucc := N.pos_pred_succ (only parsing).
 Notation Nplus_0_l := N.add_0_l (only parsing).
 Notation Nplus_0_r := N.add_0_r (only parsing).
@@ -1032,7 +1009,6 @@ Notation Nplus_comm := N.add_comm (only parsing).
 Notation Nplus_assoc := N.add_assoc (only parsing).
 Notation Nplus_succ := N.add_succ_l (only parsing).
 Notation Nsucc_0 := N.succ_0_discr (only parsing).
-Notation Nsucc_inj := N.succ_inj (compat "8.7").
 Notation Nminus_N0_Nle := N.sub_0_le (only parsing).
 Notation Nminus_0_r := N.sub_0_r (only parsing).
 Notation Nminus_succ_r:= N.sub_succ_r (only parsing).
@@ -1042,29 +1018,14 @@ Notation Nmult_1_r := N.mul_1_r (only parsing).
 Notation Nmult_comm := N.mul_comm (only parsing).
 Notation Nmult_assoc := N.mul_assoc (only parsing).
 Notation Nmult_plus_distr_r := N.mul_add_distr_r (only parsing).
-Notation Neqb_eq := N.eqb_eq (compat "8.7").
 Notation Nle_0 := N.le_0_l (only parsing).
-Notation Ncompare_refl := N.compare_refl (compat "8.7").
 Notation Ncompare_Eq_eq := N.compare_eq (only parsing).
 Notation Ncompare_eq_correct := N.compare_eq_iff (only parsing).
-Notation Nlt_irrefl := N.lt_irrefl (compat "8.7").
-Notation Nlt_trans := N.lt_trans (compat "8.7").
 Notation Nle_lteq := N.lt_eq_cases (only parsing).
-Notation Nlt_succ_r := N.lt_succ_r (compat "8.7").
-Notation Nle_trans := N.le_trans (compat "8.7").
-Notation Nle_succ_l := N.le_succ_l (compat "8.7").
-Notation Ncompare_spec := N.compare_spec (compat "8.7").
 Notation Ncompare_0 := N.compare_0_r (only parsing).
 Notation Ndouble_div2 := N.div2_double (only parsing).
 Notation Ndouble_plus_one_div2 := N.div2_succ_double (only parsing).
-Notation Ndouble_inj := N.double_inj (compat "8.7").
 Notation Ndouble_plus_one_inj := N.succ_double_inj (only parsing).
-Notation Npow_0_r := N.pow_0_r (compat "8.7").
-Notation Npow_succ_r := N.pow_succ_r (compat "8.7").
-Notation Nlog2_spec := N.log2_spec (compat "8.7").
-Notation Nlog2_nonpos := N.log2_nonpos (compat "8.7").
-Notation Neven_spec := N.even_spec (compat "8.7").
-Notation Nodd_spec := N.odd_spec (compat "8.7").
 Notation Nlt_not_eq := N.lt_neq (only parsing).
 Notation Ngt_Nlt := N.gt_lt (only parsing).
 
diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v
index e2b2b4904e..302ec434d0 100644
--- a/theories/NArith/Ndec.v
+++ b/theories/NArith/Ndec.v
@@ -22,8 +22,6 @@ Local Open Scope N_scope.
 (** Obsolete results about boolean comparisons over [N],
     kept for compatibility with IntMap and SMC. *)
 
-Notation Peqb := Pos.eqb (compat "8.7").
-Notation Neqb := N.eqb (compat "8.7").
 Notation Peqb_correct := Pos.eqb_refl (only parsing).
 Notation Neqb_correct := N.eqb_refl (only parsing).
 Notation Neqb_comm := N.eqb_sym (only parsing).
diff --git a/theories/NArith/Ndiv_def.v b/theories/NArith/Ndiv_def.v
index 885c0d48b1..9d8745fff7 100644
--- a/theories/NArith/Ndiv_def.v
+++ b/theories/NArith/Ndiv_def.v
@@ -24,10 +24,7 @@ Lemma Pdiv_eucl_remainder a b :
   snd (Pdiv_eucl a b) < Npos b.
 Proof. now apply (N.pos_div_eucl_remainder a (Npos b)). Qed.
 
-Notation Ndiv_eucl := N.div_eucl (compat "8.7").
-Notation Ndiv := N.div (compat "8.7").
 Notation Nmod := N.modulo (only parsing).
 
 Notation Ndiv_eucl_correct := N.div_eucl_spec (only parsing).
 Notation Ndiv_mod_eq := N.div_mod' (only parsing).
-Notation Nmod_lt := N.mod_lt (compat "8.7").
diff --git a/theories/NArith/Nsqrt_def.v b/theories/NArith/Nsqrt_def.v
index f043328375..3a37c94fd8 100644
--- a/theories/NArith/Nsqrt_def.v
+++ b/theories/NArith/Nsqrt_def.v
@@ -13,8 +13,4 @@ Require Import BinNat.
 (** Obsolete file, see [BinNat] now,
     only compatibility notations remain here. *)
 
-Notation Nsqrtrem := N.sqrtrem (compat "8.7").
-Notation Nsqrt := N.sqrt (compat "8.7").
-Notation Nsqrtrem_spec := N.sqrtrem_spec (compat "8.7").
 Notation Nsqrt_spec := (fun n => N.sqrt_spec n (N.le_0_l n)) (only parsing).
-Notation Nsqrtrem_sqrt := N.sqrtrem_sqrt (compat "8.7").
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 01ecdd710c..c85252d6f8 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1907,12 +1907,8 @@ Notation IsNul := Pos.IsNul (only parsing).
 Notation IsPos := Pos.IsPos (only parsing).
 Notation IsNeg := Pos.IsNeg (only parsing).
 
-Notation Psucc := Pos.succ (compat "8.7").
 Notation Pplus := Pos.add (only parsing).
 Notation Pplus_carry := Pos.add_carry (only parsing).
-Notation Ppred := Pos.pred (compat "8.7").
-Notation Piter_op := Pos.iter_op (compat "8.7").
-Notation Piter_op_succ := Pos.iter_op_succ (compat "8.7").
 Notation Pmult_nat := (Pos.iter_op plus) (only parsing).
 Notation nat_of_P := Pos.to_nat (only parsing).
 Notation P_of_succ_nat := Pos.of_succ_nat (only parsing).
@@ -1922,29 +1918,17 @@ Notation positive_mask_rect := Pos.mask_rect (only parsing).
 Notation positive_mask_ind := Pos.mask_ind (only parsing).
 Notation positive_mask_rec := Pos.mask_rec (only parsing).
 Notation Pdouble_plus_one_mask := Pos.succ_double_mask (only parsing).
-Notation Pdouble_mask := Pos.double_mask (compat "8.7").
 Notation Pdouble_minus_two := Pos.double_pred_mask (only parsing).
 Notation Pminus_mask := Pos.sub_mask (only parsing).
 Notation Pminus_mask_carry := Pos.sub_mask_carry (only parsing).
 Notation Pminus := Pos.sub (only parsing).
 Notation Pmult := Pos.mul (only parsing).
 Notation iter_pos := @Pos.iter (only parsing).
-Notation Ppow := Pos.pow (compat "8.7").
-Notation Pdiv2 := Pos.div2 (compat "8.7").
-Notation Pdiv2_up := Pos.div2_up (compat "8.7").
 Notation Psize := Pos.size_nat (only parsing).
 Notation Psize_pos := Pos.size (only parsing).
 Notation Pcompare x y m := (Pos.compare_cont m x y) (only parsing).
-Notation Plt := Pos.lt (compat "8.7").
-Notation Pgt := Pos.gt (compat "8.7").
-Notation Ple := Pos.le (compat "8.7").
-Notation Pge := Pos.ge (compat "8.7").
-Notation Pmin := Pos.min (compat "8.7").
-Notation Pmax := Pos.max (compat "8.7").
-Notation Peqb := Pos.eqb (compat "8.7").
 Notation positive_eq_dec := Pos.eq_dec (only parsing).
 Notation xI_succ_xO := Pos.xI_succ_xO (only parsing).
-Notation Psucc_discr := Pos.succ_discr (compat "8.7").
 Notation Psucc_o_double_minus_one_eq_xO :=
  Pos.succ_pred_double (only parsing).
 Notation Pdouble_minus_one_o_succ_eq_xI :=
@@ -1953,9 +1937,7 @@ Notation xO_succ_permute := Pos.double_succ (only parsing).
 Notation double_moins_un_xO_discr :=
  Pos.pred_double_xO_discr (only parsing).
 Notation Psucc_not_one := Pos.succ_not_1 (only parsing).
-Notation Ppred_succ := Pos.pred_succ (compat "8.7").
 Notation Psucc_pred := Pos.succ_pred_or (only parsing).
-Notation Psucc_inj := Pos.succ_inj (compat "8.7").
 Notation Pplus_carry_spec := Pos.add_carry_spec (only parsing).
 Notation Pplus_comm := Pos.add_comm (only parsing).
 Notation Pplus_succ_permute_r := Pos.add_succ_r (only parsing).
@@ -2002,17 +1984,11 @@ Notation Pmult_xO_discr := Pos.mul_xO_discr (only parsing).
 Notation Pmult_reg_r := Pos.mul_reg_r (only parsing).
 Notation Pmult_reg_l := Pos.mul_reg_l (only parsing).
 Notation Pmult_1_inversion_l := Pos.mul_eq_1_l (only parsing).
-Notation Psquare_xO := Pos.square_xO (compat "8.7").
-Notation Psquare_xI := Pos.square_xI (compat "8.7").
 Notation iter_pos_swap_gen := Pos.iter_swap_gen (only parsing).
 Notation iter_pos_swap := Pos.iter_swap (only parsing).
 Notation iter_pos_succ := Pos.iter_succ (only parsing).
 Notation iter_pos_plus := Pos.iter_add (only parsing).
 Notation iter_pos_invariant := Pos.iter_invariant (only parsing).
-Notation Ppow_1_r := Pos.pow_1_r (compat "8.7").
-Notation Ppow_succ_r := Pos.pow_succ_r (compat "8.7").
-Notation Peqb_refl := Pos.eqb_refl (compat "8.7").
-Notation Peqb_eq := Pos.eqb_eq (compat "8.7").
 Notation Pcompare_refl_id := Pos.compare_cont_refl (only parsing).
 Notation Pcompare_eq_iff := Pos.compare_eq_iff (only parsing).
 Notation Pcompare_Gt_Lt := Pos.compare_cont_Gt_Lt (only parsing).
@@ -2022,23 +1998,9 @@ Notation Pcompare_Lt_Gt := Pos.compare_cont_Lt_Gt (only parsing).
 Notation Pcompare_antisym := Pos.compare_cont_antisym (only parsing).
 Notation ZC1 := Pos.gt_lt (only parsing).
 Notation ZC2 := Pos.lt_gt (only parsing).
-Notation Pcompare_spec := Pos.compare_spec (compat "8.7").
 Notation Pcompare_p_Sp := Pos.lt_succ_diag_r (only parsing).
-Notation Pcompare_succ_succ := Pos.compare_succ_succ (compat "8.7").
 Notation Pcompare_1 := Pos.nlt_1_r (only parsing).
 Notation Plt_1 := Pos.nlt_1_r (only parsing).
-Notation Plt_1_succ := Pos.lt_1_succ (compat "8.7").
-Notation Plt_lt_succ := Pos.lt_lt_succ (compat "8.7").
-Notation Plt_irrefl := Pos.lt_irrefl (compat "8.7").
-Notation Plt_trans := Pos.lt_trans (compat "8.7").
-Notation Plt_ind := Pos.lt_ind (compat "8.7").
-Notation Ple_lteq := Pos.le_lteq (compat "8.7").
-Notation Ple_refl := Pos.le_refl (compat "8.7").
-Notation Ple_lt_trans := Pos.le_lt_trans (compat "8.7").
-Notation Plt_le_trans := Pos.lt_le_trans (compat "8.7").
-Notation Ple_trans := Pos.le_trans (compat "8.7").
-Notation Plt_succ_r := Pos.lt_succ_r (compat "8.7").
-Notation Ple_succ_l := Pos.le_succ_l (compat "8.7").
 Notation Pplus_compare_mono_l := Pos.add_compare_mono_l (only parsing).
 Notation Pplus_compare_mono_r := Pos.add_compare_mono_r (only parsing).
 Notation Pplus_lt_mono_l := Pos.add_lt_mono_l (only parsing).
@@ -2057,8 +2019,6 @@ Notation Pmult_le_mono_r := Pos.mul_le_mono_r (only parsing).
 Notation Pmult_le_mono := Pos.mul_le_mono (only parsing).
 Notation Plt_plus_r := Pos.lt_add_r (only parsing).
 Notation Plt_not_plus_l := Pos.lt_not_add_l (only parsing).
-Notation Ppow_gt_1 := Pos.pow_gt_1 (compat "8.7").
-Notation Ppred_mask := Pos.pred_mask (compat "8.7").
 Notation Pminus_mask_succ_r := Pos.sub_mask_succ_r (only parsing).
 Notation Pminus_mask_carry_spec := Pos.sub_mask_carry_spec (only parsing).
 Notation Pminus_succ_r := Pos.sub_succ_r (only parsing).
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 542d169e66..a346ab8ccb 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1612,40 +1612,18 @@ End Z2Pos.
 
 Notation Zdouble_plus_one := Z.succ_double (only parsing).
 Notation Zdouble_minus_one := Z.pred_double (only parsing).
-Notation Zdouble := Z.double (compat "8.7").
 Notation ZPminus := Z.pos_sub (only parsing).
-Notation Zsucc' := Z.succ (compat "8.7").
-Notation Zpred' := Z.pred (compat "8.7").
-Notation Zplus' := Z.add (compat "8.7").
 Notation Zplus := Z.add (only parsing). (* Slightly incompatible *)
-Notation Zopp := Z.opp (compat "8.7").
-Notation Zsucc := Z.succ (compat "8.7").
-Notation Zpred := Z.pred (compat "8.7").
 Notation Zminus := Z.sub (only parsing).
 Notation Zmult := Z.mul (only parsing).
-Notation Zcompare := Z.compare (compat "8.7").
-Notation Zsgn := Z.sgn (compat "8.7").
-Notation Zle := Z.le (compat "8.7").
-Notation Zge := Z.ge (compat "8.7").
-Notation Zlt := Z.lt (compat "8.7").
-Notation Zgt := Z.gt (compat "8.7").
-Notation Zmax := Z.max (compat "8.7").
-Notation Zmin := Z.min (compat "8.7").
-Notation Zabs := Z.abs (compat "8.7").
-Notation Zabs_nat := Z.abs_nat (compat "8.7").
-Notation Zabs_N := Z.abs_N (compat "8.7").
 Notation Z_of_nat := Z.of_nat (only parsing).
 Notation Z_of_N := Z.of_N (only parsing).
 
 Notation Zind := Z.peano_ind (only parsing).
-Notation Zopp_0 := Z.opp_0 (compat "8.7").
-Notation Zopp_involutive := Z.opp_involutive (compat "8.7").
-Notation Zopp_inj := Z.opp_inj (compat "8.7").
 Notation Zplus_0_l := Z.add_0_l (only parsing).
 Notation Zplus_0_r := Z.add_0_r (only parsing).
 Notation Zplus_comm := Z.add_comm (only parsing).
 Notation Zopp_plus_distr := Z.opp_add_distr (only parsing).
-Notation Zopp_succ := Z.opp_succ (compat "8.7").
 Notation Zplus_opp_r := Z.add_opp_diag_r (only parsing).
 Notation Zplus_opp_l := Z.add_opp_diag_l (only parsing).
 Notation Zplus_assoc := Z.add_assoc (only parsing).
@@ -1654,11 +1632,6 @@ Notation Zplus_reg_l := Z.add_reg_l (only parsing).
 Notation Zplus_succ_l := Z.add_succ_l (only parsing).
 Notation Zplus_succ_comm := Z.add_succ_comm (only parsing).
 Notation Zsucc_discr := Z.neq_succ_diag_r (only parsing).
-Notation Zsucc_inj := Z.succ_inj (compat "8.7").
-Notation Zsucc'_inj := Z.succ_inj (compat "8.7").
-Notation Zsucc'_pred' := Z.succ_pred (compat "8.7").
-Notation Zpred'_succ' := Z.pred_succ (compat "8.7").
-Notation Zpred'_inj := Z.pred_inj (compat "8.7").
 Notation Zsucc'_discr := Z.neq_succ_diag_r (only parsing).
 Notation Zminus_0_r := Z.sub_0_r (only parsing).
 Notation Zminus_diag := Z.sub_diag (only parsing).
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index 6cadf30f85..88288d3964 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -34,8 +34,6 @@ Lemma Zcompare_rec (P:Set) (n m:Z) :
   ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P.
 Proof. apply Zcompare_rect. Defined.
 
-Notation Z_eq_dec := Z.eq_dec (compat "8.7").
-
 Section decidability.
 
   Variables x y : Z.
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index 057eb49965..d926198a9c 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -29,17 +29,13 @@ Local Open Scope Z_scope.
 (**********************************************************************)
 (** * Properties of absolute value *)
 
-Notation Zabs_eq := Z.abs_eq (compat "8.7").
 Notation Zabs_non_eq := Z.abs_neq (only parsing).
 Notation Zabs_Zopp := Z.abs_opp (only parsing).
 Notation Zabs_pos := Z.abs_nonneg (only parsing).
-Notation Zabs_involutive := Z.abs_involutive (compat "8.7").
 Notation Zabs_eq_case := Z.abs_eq_cases (only parsing).
-Notation Zabs_triangle := Z.abs_triangle (compat "8.7").
 Notation Zsgn_Zabs := Z.sgn_abs (only parsing).
 Notation Zabs_Zsgn := Z.abs_sgn (only parsing).
 Notation Zabs_Zmult := Z.abs_mul (only parsing).
-Notation Zabs_square := Z.abs_square (compat "8.7").
 
 (** * Proving a property of the absolute value by cases *)
 
diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v
index 6ccb0153de..eec3878898 100644
--- a/theories/ZArith/Zcompare.v
+++ b/theories/ZArith/Zcompare.v
@@ -183,15 +183,8 @@ Qed.
 
 (** Compatibility notations *)
 
-Notation Zcompare_refl := Z.compare_refl (compat "8.7").
 Notation Zcompare_Eq_eq := Z.compare_eq (only parsing).
 Notation Zcompare_Eq_iff_eq := Z.compare_eq_iff (only parsing).
-Notation Zcompare_spec := Z.compare_spec (compat "8.7").
-Notation Zmin_l := Z.min_l (compat "8.7").
-Notation Zmin_r := Z.min_r (compat "8.7").
-Notation Zmax_l := Z.max_l (compat "8.7").
-Notation Zmax_r := Z.max_r (compat "8.7").
-Notation Zabs_eq := Z.abs_eq (compat "8.7").
 Notation Zabs_non_eq := Z.abs_neq (only parsing).
 Notation Zsgn_0 := Z.sgn_null (only parsing).
 Notation Zsgn_1 := Z.sgn_pos (only parsing).
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index c278cada61..8b69fb04f4 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -21,11 +21,8 @@ Local Open Scope Z_scope.
     specifications and properties are in [BinInt]. *)
 
 Notation Zdiv_eucl_POS := Z.pos_div_eucl (only parsing).
-Notation Zdiv_eucl := Z.div_eucl (compat "8.7").
-Notation Zdiv := Z.div (compat "8.7").
 Notation Zmod := Z.modulo (only parsing).
 
-Notation Zdiv_eucl_eq := Z.div_eucl_eq (compat "8.7").
 Notation Z_div_mod_eq_full := Z.div_mod (only parsing).
 Notation Zmod_POS_bound := Z.pos_div_eucl_bound (only parsing).
 Notation Zmod_pos_bound := Z.mod_pos_bound (only parsing).
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index 9e83bfc136..45d0f58524 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -141,9 +141,6 @@ Notation Zodd_bool_pred := Z.odd_pred (only parsing).
 (** * Definition of [Z.quot2], [Z.div2] and properties wrt [Zeven]
   and [Zodd] *)
 
-Notation Zdiv2 := Z.div2 (compat "8.7").
-Notation Zquot2 := Z.quot2 (compat "8.7").
-
 (** Properties of [Z.div2] *)
 
 Lemma Zdiv2_odd_eqn n : n = 2*(Z.div2 n) + if Z.odd n then 1 else 0.
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index 26bd9e8171..08d4de0d1e 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -18,22 +18,13 @@ Local Open Scope Z_scope.
 
 (** Exact compatibility *)
 
-Notation Zmax_case := Z.max_case (compat "8.7").
-Notation Zmax_case_strong := Z.max_case_strong (compat "8.7").
 Notation Zmax_right := Z.max_r (only parsing).
-Notation Zle_max_l := Z.le_max_l (compat "8.7").
-Notation Zle_max_r := Z.le_max_r (compat "8.7").
-Notation Zmax_lub := Z.max_lub (compat "8.7").
-Notation Zmax_lub_lt := Z.max_lub_lt (compat "8.7").
 Notation Zle_max_compat_r := Z.max_le_compat_r (only parsing).
 Notation Zle_max_compat_l := Z.max_le_compat_l (only parsing).
 Notation Zmax_idempotent := Z.max_id (only parsing).
 Notation Zmax_n_n := Z.max_id (only parsing).
-Notation Zmax_comm := Z.max_comm (compat "8.7").
-Notation Zmax_assoc := Z.max_assoc (compat "8.7").
 Notation Zmax_irreducible_dec := Z.max_dec (only parsing).
 Notation Zmax_le_prime := Z.max_le (only parsing).
-Notation Zsucc_max_distr := Z.succ_max_distr (compat "8.7").
 Notation Zmax_SS := Z.succ_max_distr (only parsing).
 Notation Zplus_max_distr_l := Z.add_max_distr_l (only parsing).
 Notation Zplus_max_distr_r := Z.add_max_distr_r (only parsing).
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index 5509ee7865..b56f563e0e 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -18,20 +18,11 @@ Local Open Scope Z_scope.
 
 (** Exact compatibility *)
 
-Notation Zmin_case := Z.min_case (compat "8.7").
-Notation Zmin_case_strong := Z.min_case_strong (compat "8.7").
-Notation Zle_min_l := Z.le_min_l (compat "8.7").
-Notation Zle_min_r := Z.le_min_r (compat "8.7").
-Notation Zmin_glb := Z.min_glb (compat "8.7").
-Notation Zmin_glb_lt := Z.min_glb_lt (compat "8.7").
 Notation Zle_min_compat_r := Z.min_le_compat_r (only parsing).
 Notation Zle_min_compat_l := Z.min_le_compat_l (only parsing).
 Notation Zmin_idempotent := Z.min_id (only parsing).
 Notation Zmin_n_n := Z.min_id (only parsing).
-Notation Zmin_comm := Z.min_comm (compat "8.7").
-Notation Zmin_assoc := Z.min_assoc (compat "8.7").
 Notation Zmin_irreducible_inf := Z.min_dec (only parsing).
-Notation Zsucc_min_distr := Z.succ_min_distr (compat "8.7").
 Notation Zmin_SS := Z.succ_min_distr (only parsing).
 Notation Zplus_min_distr_r := Z.add_min_distr_r (only parsing).
 Notation Zmin_plus := Z.add_min_distr_r (only parsing).
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index e6066d53f9..7191825af0 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -27,28 +27,15 @@ Open Scope Z_scope.
      - properties of the efficient [Z.gcd] function
 *)
 
-Notation Zgcd := Z.gcd (compat "8.7").
-Notation Zggcd := Z.ggcd (compat "8.7").
-Notation Zggcd_gcd := Z.ggcd_gcd (compat "8.7").
-Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (compat "8.7").
-Notation Zgcd_divide_l := Z.gcd_divide_l (compat "8.7").
-Notation Zgcd_divide_r := Z.gcd_divide_r (compat "8.7").
-Notation Zgcd_greatest := Z.gcd_greatest (compat "8.7").
-Notation Zgcd_nonneg := Z.gcd_nonneg (compat "8.7").
-Notation Zggcd_opp := Z.ggcd_opp (compat "8.7").
-
 (** The former specialized inductive predicate [Z.divide] is now
     a generic existential predicate. *)
 
-Notation Zdivide := Z.divide (compat "8.7").
-
 (** Its former constructor is now a pseudo-constructor. *)
 
 Definition Zdivide_intro a b q (H:b=q*a) : Z.divide a b := ex_intro _ q H.
 
 (** Results concerning divisibility*)
 
-Notation Zdivide_refl := Z.divide_refl (compat "8.7").
 Notation Zone_divide := Z.divide_1_l (only parsing).
 Notation Zdivide_0 := Z.divide_0_r (only parsing).
 Notation Zmult_divide_compat_l := Z.mul_divide_mono_l (only parsing).
@@ -95,11 +82,6 @@ Qed.
 
 Notation Zdivide_1 := Z.divide_1_r (only parsing).
 
-(** If [a] divides [b] and [b] divides [a] then [a] is [b] or [-b]. *)
-
-Notation Zdivide_antisym := Z.divide_antisym (compat "8.7").
-Notation Zdivide_trans := Z.divide_trans (compat "8.7").
-
 (** If [a] divides [b] and [b<>0] then [|a| <= |b|]. *)
 
 Lemma Zdivide_bounds a b : (a | b) -> b <> 0 -> Z.abs a <= Z.abs b.
@@ -800,8 +782,6 @@ Proof.
   rewrite <- Zdivide_Zdiv_eq; auto.
 Qed.
 
-Notation Zgcd_comm := Z.gcd_comm (compat "8.7").
-
 Lemma Zgcd_ass a b c : Z.gcd (Z.gcd a b) c = Z.gcd a (Z.gcd b c).
 Proof.
  symmetry. apply Z.gcd_assoc.
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index bd460f77f0..9911a568cc 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -71,10 +71,6 @@ Register not_Zeq as plugins.omega.not_Zeq.
 
 (** * Relating strict and large orders *)
 
-Notation Zgt_lt := Z.gt_lt (compat "8.7").
-Notation Zlt_gt := Z.lt_gt (compat "8.7").
-Notation Zge_le := Z.ge_le (compat "8.7").
-Notation Zle_ge := Z.le_ge (compat "8.7").
 Notation Zgt_iff_lt := Z.gt_lt_iff (only parsing).
 Notation Zge_iff_le := Z.ge_le_iff (only parsing).
 
@@ -134,7 +130,6 @@ Register not_Zne as plugins.omega.not_Zne.
 
 (** Reflexivity *)
 
-Notation Zle_refl := Z.le_refl (compat "8.7").
 Notation Zeq_le := Z.eq_le_incl (only parsing).
 
 Hint Resolve Z.le_refl: zarith.
@@ -154,7 +149,6 @@ Qed.
 
 (** Irreflexivity *)
 
-Notation Zlt_irrefl := Z.lt_irrefl (compat "8.7").
 Notation Zlt_not_eq := Z.lt_neq (only parsing).
 
 Lemma Zgt_irrefl n : ~ n > n.
@@ -178,8 +172,6 @@ Notation Zle_or_lt := Z.le_gt_cases (only parsing).
 
 (** Transitivity of strict orders *)
 
-Notation Zlt_trans := Z.lt_trans (compat "8.7").
-
 Lemma Zgt_trans n m p : n > m -> m > p -> n > p.
 Proof.
   Z.swap_greater. intros; now transitivity m.
@@ -187,9 +179,6 @@ Qed.
 
 (** Mixed transitivity *)
 
-Notation Zlt_le_trans := Z.lt_le_trans (compat "8.7").
-Notation Zle_lt_trans := Z.le_lt_trans (compat "8.7").
-
 Lemma Zle_gt_trans n m p : m <= n -> m > p -> n > p.
 Proof.
   Z.swap_greater. Z.order.
@@ -202,8 +191,6 @@ Qed.
 
 (** Transitivity of large orders *)
 
-Notation Zle_trans := Z.le_trans (compat "8.7").
-
 Lemma Zge_trans n m p : n >= m -> m >= p -> n >= p.
 Proof.
   Z.swap_greater. Z.order.
@@ -268,9 +255,6 @@ Qed.
 
 (** Relating strict and large order using successor or predecessor *)
 
-Notation Zlt_succ_r := Z.lt_succ_r (compat "8.7").
-Notation Zle_succ_l := Z.le_succ_l (compat "8.7").
-
 Lemma Zgt_le_succ n m : m > n -> Z.succ n <= m.
 Proof.
   Z.swap_greater. apply Z.le_succ_l.
@@ -347,9 +331,6 @@ Qed.
 
 (** Special cases of ordered integers *)
 
-Notation Zlt_0_1 := Z.lt_0_1 (compat "8.7").
-Notation Zle_0_1 := Z.le_0_1 (compat "8.7").
-
 Lemma Zle_neg_pos : forall p q:positive, Zneg p <= Zpos q.
 Proof.
   exact Pos2Z.neg_le_pos.
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index 881ead1c4b..6e4850338a 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -233,7 +233,5 @@ Qed.
 
 (** * Z.square: a direct definition of [z^2] *)
 
-Notation Psquare := Pos.square (compat "8.7").
-Notation Zsquare := Z.square (compat "8.7").
 Notation Psquare_correct := Pos.square_spec (only parsing).
 Notation Zsquare_correct := Z.square_spec (only parsing).
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
index 264109dc6f..a619eb90ef 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -37,17 +37,7 @@ Notation Ndiv_Zquot := N2Z.inj_quot (only parsing).
 Notation Nmod_Zrem := N2Z.inj_rem (only parsing).
 Notation Z_quot_rem_eq := Z.quot_rem' (only parsing).
 Notation Zrem_lt := Z.rem_bound_abs (only parsing).
-Notation Zquot_unique := Z.quot_unique (compat "8.7").
-Notation Zrem_unique := Z.rem_unique (compat "8.7").
-Notation Zrem_1_r := Z.rem_1_r (compat "8.7").
-Notation Zquot_1_r := Z.quot_1_r (compat "8.7").
-Notation Zrem_1_l := Z.rem_1_l (compat "8.7").
-Notation Zquot_1_l := Z.quot_1_l (compat "8.7").
-Notation Z_quot_same := Z.quot_same (compat "8.7").
 Notation Z_quot_mult := Z.quot_mul (only parsing).
-Notation Zquot_small := Z.quot_small (compat "8.7").
-Notation Zrem_small := Z.rem_small (compat "8.7").
-Notation Zquot2_quot := Zquot2_quot (compat "8.7").
 
 (** Particular values taken for [a÷0] and [(Z.rem a 0)].
     We avise to not rely on these arbitrary values. *)
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index d682d3641f..bf1297d661 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -155,7 +155,6 @@ let add_vo_require opts d p export =
 
 let add_compat_require opts v =
   match v with
-  | Flags.V8_7 -> add_vo_require opts "Coq.Compat.Coq87" None (Some false)
   | Flags.V8_8 -> add_vo_require opts "Coq.Compat.Coq88" None (Some false)
   | Flags.V8_9 -> add_vo_require opts "Coq.Compat.Coq89" None (Some false)
   | Flags.Current -> add_vo_require opts "Coq.Compat.Coq810" None (Some false)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 589b15fd41..2853d6e65f 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -65,8 +65,7 @@ let parse_compat_version = let open Flags in function
   | "8.10" -> Current
   | "8.9" -> V8_9
   | "8.8" -> V8_8
-  | "8.7" -> V8_7
-  | ("8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
+  | ("8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
     CErrors.user_err ~hdr:"get_compat_version"
       Pp.(str "Compatibility with version " ++ str s ++ str " not supported.")
   | s ->