Remove -compat 8.7

This removes various compatibility notations.

Closes #8374

This commit was mostly created by running `./dev/tools/update-compat.py
--release`.  There's a bit of manual spacing adjustment around all of the
removed compatibility notations, and some test-suite updates were done
manually.

The update to CHANGES.md was manual.

4 files changed, 0 insertions, 48 deletions

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").