Update compat notations to be compat 8.7

All changes done with

```
git grep --name-only 'compat "8.6"' | xargs sed -i s'/compat "8.6"/compat "8.7"/g'
```

As per https://github.com/coq/coq/pull/8374#issuecomment-426202818 and
https://github.com/coq/coq/issues/8383#issuecomment-426200497

21 files changed, 208 insertions, 208 deletions

diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 713aef858e..6f220f2023 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -135,10 +135,10 @@ Qed.
     See now [Nat.compare] and its properties.
     In scope [nat_scope], the notation for [Nat.compare] is "?=" *)
 
-Notation nat_compare := Nat.compare (compat "8.6").
+Notation nat_compare := Nat.compare (compat "8.7").
 
-Notation nat_compare_spec := Nat.compare_spec (compat "8.6").
-Notation nat_compare_eq_iff := Nat.compare_eq_iff (compat "8.6").
+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/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 997059669d..2d5a79838a 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -26,7 +26,7 @@ Hint Extern 1 (Equivalence _) => constructor; congruence.
 
 Module WFacts_fun (E:DecidableType)(Import M:WSfun E).
 
-Notation option_map := option_map (compat "8.6").
+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.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index d6a0fb214f..a5f926f7ab 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -782,16 +782,16 @@ Hint Resolve exist exist2 existT existT2: core.
 
 (* Compatibility *)
 
-Notation sigS := sigT (compat "8.6").
-Notation existS := existT (compat "8.6").
-Notation sigS_rect := sigT_rect (compat "8.6").
-Notation sigS_rec := sigT_rec (compat "8.6").
-Notation sigS_ind := sigT_ind (compat "8.6").
-Notation projS1 := projT1 (compat "8.6").
-Notation projS2 := projT2 (compat "8.6").
-
-Notation sigS2 := sigT2 (compat "8.6").
-Notation existS2 := existT2 (compat "8.6").
-Notation sigS2_rect := sigT2_rect (compat "8.6").
-Notation sigS2_rec := sigT2_rec (compat "8.6").
-Notation sigS2_ind := sigT2_ind (compat "8.6").
+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 d938b315f1..8e59941f37 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -125,7 +125,7 @@ Proof.
   apply eq_dep_intro.
 Qed.
 
-Notation eq_sigS_eq_dep := eq_sigT_eq_dep (compat "8.6"). (* Compatibility *)
+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),
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index bd27f94abd..92c124ec32 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -966,33 +966,33 @@ Notation N_ind := N_ind (only parsing).
 Notation N0 := N0 (only parsing).
 Notation Npos := N.pos (only parsing).
 
-Notation Ndiscr := N.discr (compat "8.6").
+Notation Ndiscr := N.discr (compat "8.7").
 Notation Ndouble_plus_one := N.succ_double (only parsing).
-Notation Ndouble := N.double (compat "8.6").
-Notation Nsucc := N.succ (compat "8.6").
-Notation Npred := N.pred (compat "8.6").
-Notation Nsucc_pos := N.succ_pos (compat "8.6").
-Notation Ppred_N := Pos.pred_N (compat "8.6").
+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.6").
-Notation Ncompare := N.compare (compat "8.6").
-Notation Nlt := N.lt (compat "8.6").
-Notation Ngt := N.gt (compat "8.6").
-Notation Nle := N.le (compat "8.6").
-Notation Nge := N.ge (compat "8.6").
-Notation Nmin := N.min (compat "8.6").
-Notation Nmax := N.max (compat "8.6").
-Notation Ndiv2 := N.div2 (compat "8.6").
-Notation Neven := N.even (compat "8.6").
-Notation Nodd := N.odd (compat "8.6").
-Notation Npow := N.pow (compat "8.6").
-Notation Nlog2 := N.log2 (compat "8.6").
+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.6").
+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).
@@ -1001,11 +1001,11 @@ 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.6").
+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.6").
+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.6").
+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).
@@ -1013,7 +1013,7 @@ 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.6").
+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).
@@ -1023,29 +1023,29 @@ 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.6").
+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.6").
+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.6").
-Notation Nlt_trans := N.lt_trans (compat "8.6").
+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.6").
-Notation Nle_trans := N.le_trans (compat "8.6").
-Notation Nle_succ_l := N.le_succ_l (compat "8.6").
-Notation Ncompare_spec := N.compare_spec (compat "8.6").
+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.6").
+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.6").
-Notation Npow_succ_r := N.pow_succ_r (compat "8.6").
-Notation Nlog2_spec := N.log2_spec (compat "8.6").
-Notation Nlog2_nonpos := N.log2_nonpos (compat "8.6").
-Notation Neven_spec := N.even_spec (compat "8.6").
-Notation Nodd_spec := N.odd_spec (compat "8.6").
+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 67c30f2250..e2b2b4904e 100644
--- a/theories/NArith/Ndec.v
+++ b/theories/NArith/Ndec.v
@@ -22,8 +22,8 @@ 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.6").
-Notation Neqb := N.eqb (compat "8.6").
+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 7c9fd86958..885c0d48b1 100644
--- a/theories/NArith/Ndiv_def.v
+++ b/theories/NArith/Ndiv_def.v
@@ -24,10 +24,10 @@ 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.6").
-Notation Ndiv := N.div (compat "8.6").
+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.6").
+Notation Nmod_lt := N.mod_lt (compat "8.7").
diff --git a/theories/NArith/Nsqrt_def.v b/theories/NArith/Nsqrt_def.v
index e771fe9167..f043328375 100644
--- a/theories/NArith/Nsqrt_def.v
+++ b/theories/NArith/Nsqrt_def.v
@@ -13,8 +13,8 @@ Require Import BinNat.
 (** Obsolete file, see [BinNat] now,
     only compatibility notations remain here. *)
 
-Notation Nsqrtrem := N.sqrtrem (compat "8.6").
-Notation Nsqrt := N.sqrt (compat "8.6").
-Notation Nsqrtrem_spec := N.sqrtrem_spec (compat "8.6").
+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.6").
+Notation Nsqrtrem_sqrt := N.sqrtrem_sqrt (compat "8.7").
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index dcaae1606d..01ecdd710c 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1907,12 +1907,12 @@ Notation IsNul := Pos.IsNul (only parsing).
 Notation IsPos := Pos.IsPos (only parsing).
 Notation IsNeg := Pos.IsNeg (only parsing).
 
-Notation Psucc := Pos.succ (compat "8.6").
+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.6").
-Notation Piter_op := Pos.iter_op (compat "8.6").
-Notation Piter_op_succ := Pos.iter_op_succ (compat "8.6").
+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 +1922,29 @@ 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.6").
+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.6").
-Notation Pdiv2 := Pos.div2 (compat "8.6").
-Notation Pdiv2_up := Pos.div2_up (compat "8.6").
+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.6").
-Notation Pgt := Pos.gt (compat "8.6").
-Notation Ple := Pos.le (compat "8.6").
-Notation Pge := Pos.ge (compat "8.6").
-Notation Pmin := Pos.min (compat "8.6").
-Notation Pmax := Pos.max (compat "8.6").
-Notation Peqb := Pos.eqb (compat "8.6").
+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.6").
+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 +1953,9 @@ 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.6").
+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.6").
+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 +2002,17 @@ 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.6").
-Notation Psquare_xI := Pos.square_xI (compat "8.6").
+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.6").
-Notation Ppow_succ_r := Pos.pow_succ_r (compat "8.6").
-Notation Peqb_refl := Pos.eqb_refl (compat "8.6").
-Notation Peqb_eq := Pos.eqb_eq (compat "8.6").
+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 +2022,23 @@ 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.6").
+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.6").
+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.6").
-Notation Plt_lt_succ := Pos.lt_lt_succ (compat "8.6").
-Notation Plt_irrefl := Pos.lt_irrefl (compat "8.6").
-Notation Plt_trans := Pos.lt_trans (compat "8.6").
-Notation Plt_ind := Pos.lt_ind (compat "8.6").
-Notation Ple_lteq := Pos.le_lteq (compat "8.6").
-Notation Ple_refl := Pos.le_refl (compat "8.6").
-Notation Ple_lt_trans := Pos.le_lt_trans (compat "8.6").
-Notation Plt_le_trans := Pos.lt_le_trans (compat "8.6").
-Notation Ple_trans := Pos.le_trans (compat "8.6").
-Notation Plt_succ_r := Pos.lt_succ_r (compat "8.6").
-Notation Ple_succ_l := Pos.le_succ_l (compat "8.6").
+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 +2057,8 @@ 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.6").
-Notation Ppred_mask := Pos.pred_mask (compat "8.6").
+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 a11d491a8b..1241345338 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1571,40 +1571,40 @@ 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.6").
+Notation Zdouble := Z.double (compat "8.7").
 Notation ZPminus := Z.pos_sub (only parsing).
-Notation Zsucc' := Z.succ (compat "8.6").
-Notation Zpred' := Z.pred (compat "8.6").
-Notation Zplus' := Z.add (compat "8.6").
+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.6").
-Notation Zsucc := Z.succ (compat "8.6").
-Notation Zpred := Z.pred (compat "8.6").
+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.6").
-Notation Zsgn := Z.sgn (compat "8.6").
-Notation Zle := Z.le (compat "8.6").
-Notation Zge := Z.ge (compat "8.6").
-Notation Zlt := Z.lt (compat "8.6").
-Notation Zgt := Z.gt (compat "8.6").
-Notation Zmax := Z.max (compat "8.6").
-Notation Zmin := Z.min (compat "8.6").
-Notation Zabs := Z.abs (compat "8.6").
-Notation Zabs_nat := Z.abs_nat (compat "8.6").
-Notation Zabs_N := Z.abs_N (compat "8.6").
+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.6").
-Notation Zopp_involutive := Z.opp_involutive (compat "8.6").
-Notation Zopp_inj := Z.opp_inj (compat "8.6").
+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.6").
+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).
@@ -1613,11 +1613,11 @@ 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.6").
-Notation Zsucc'_inj := Z.succ_inj (compat "8.6").
-Notation Zsucc'_pred' := Z.succ_pred (compat "8.6").
-Notation Zpred'_succ' := Z.pred_succ (compat "8.6").
-Notation Zpred'_inj := Z.pred_inj (compat "8.6").
+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 9bcdb73afa..6cadf30f85 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -34,7 +34,7 @@ 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.6").
+Notation Z_eq_dec := Z.eq_dec (compat "8.7").
 
 Section decidability.
 
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index 0d8450e36b..057eb49965 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -29,17 +29,17 @@ Local Open Scope Z_scope.
 (**********************************************************************)
 (** * Properties of absolute value *)
 
-Notation Zabs_eq := Z.abs_eq (compat "8.6").
+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.6").
+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.6").
+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.6").
+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 c8432e27bb..6ccb0153de 100644
--- a/theories/ZArith/Zcompare.v
+++ b/theories/ZArith/Zcompare.v
@@ -183,15 +183,15 @@ Qed.
 
 (** Compatibility notations *)
 
-Notation Zcompare_refl := Z.compare_refl (compat "8.6").
+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.6").
-Notation Zmin_l := Z.min_l (compat "8.6").
-Notation Zmin_r := Z.min_r (compat "8.6").
-Notation Zmax_l := Z.max_l (compat "8.6").
-Notation Zmax_r := Z.max_r (compat "8.6").
-Notation Zabs_eq := Z.abs_eq (compat "8.6").
+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 15d0e48747..74614e114a 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -21,11 +21,11 @@ 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.6").
-Notation Zdiv := Z.div (compat "8.6").
+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.6").
+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 00a58b517e..9e83bfc136 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -141,8 +141,8 @@ 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.6").
-Notation Zquot2 := Z.quot2 (compat "8.6").
+Notation Zdiv2 := Z.div2 (compat "8.7").
+Notation Zquot2 := Z.quot2 (compat "8.7").
 
 (** Properties of [Z.div2] *)
 
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index 7f595fcfd0..26bd9e8171 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -18,22 +18,22 @@ Local Open Scope Z_scope.
 
 (** Exact compatibility *)
 
-Notation Zmax_case := Z.max_case (compat "8.6").
-Notation Zmax_case_strong := Z.max_case_strong (compat "8.6").
+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.6").
-Notation Zle_max_r := Z.le_max_r (compat "8.6").
-Notation Zmax_lub := Z.max_lub (compat "8.6").
-Notation Zmax_lub_lt := Z.max_lub_lt (compat "8.6").
+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.6").
-Notation Zmax_assoc := Z.max_assoc (compat "8.6").
+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.6").
+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 6bc72227b2..5509ee7865 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -18,20 +18,20 @@ Local Open Scope Z_scope.
 
 (** Exact compatibility *)
 
-Notation Zmin_case := Z.min_case (compat "8.6").
-Notation Zmin_case_strong := Z.min_case_strong (compat "8.6").
-Notation Zle_min_l := Z.le_min_l (compat "8.6").
-Notation Zle_min_r := Z.le_min_r (compat "8.6").
-Notation Zmin_glb := Z.min_glb (compat "8.6").
-Notation Zmin_glb_lt := Z.min_glb_lt (compat "8.6").
+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.6").
-Notation Zmin_assoc := Z.min_assoc (compat "8.6").
+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.6").
+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 f5444c31d7..e6066d53f9 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -27,20 +27,20 @@ Open Scope Z_scope.
      - properties of the efficient [Z.gcd] function
 *)
 
-Notation Zgcd := Z.gcd (compat "8.6").
-Notation Zggcd := Z.ggcd (compat "8.6").
-Notation Zggcd_gcd := Z.ggcd_gcd (compat "8.6").
-Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (compat "8.6").
-Notation Zgcd_divide_l := Z.gcd_divide_l (compat "8.6").
-Notation Zgcd_divide_r := Z.gcd_divide_r (compat "8.6").
-Notation Zgcd_greatest := Z.gcd_greatest (compat "8.6").
-Notation Zgcd_nonneg := Z.gcd_nonneg (compat "8.6").
-Notation Zggcd_opp := Z.ggcd_opp (compat "8.6").
+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.6").
+Notation Zdivide := Z.divide (compat "8.7").
 
 (** Its former constructor is now a pseudo-constructor. *)
 
@@ -48,7 +48,7 @@ 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.6").
+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).
@@ -97,8 +97,8 @@ 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.6").
-Notation Zdivide_trans := Z.divide_trans (compat "8.6").
+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|]. *)
 
@@ -800,7 +800,7 @@ Proof.
   rewrite <- Zdivide_Zdiv_eq; auto.
 Qed.
 
-Notation Zgcd_comm := Z.gcd_comm (compat "8.6").
+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.
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index a1ec4b35e0..208e84aeb7 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -66,10 +66,10 @@ Qed.
 
 (** * Relating strict and large orders *)
 
-Notation Zgt_lt := Z.gt_lt (compat "8.6").
-Notation Zlt_gt := Z.lt_gt (compat "8.6").
-Notation Zge_le := Z.ge_le (compat "8.6").
-Notation Zle_ge := Z.le_ge (compat "8.6").
+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).
 
@@ -123,7 +123,7 @@ Qed.
 
 (** Reflexivity *)
 
-Notation Zle_refl := Z.le_refl (compat "8.6").
+Notation Zle_refl := Z.le_refl (compat "8.7").
 Notation Zeq_le := Z.eq_le_incl (only parsing).
 
 Hint Resolve Z.le_refl: zarith.
@@ -143,7 +143,7 @@ Qed.
 
 (** Irreflexivity *)
 
-Notation Zlt_irrefl := Z.lt_irrefl (compat "8.6").
+Notation Zlt_irrefl := Z.lt_irrefl (compat "8.7").
 Notation Zlt_not_eq := Z.lt_neq (only parsing).
 
 Lemma Zgt_irrefl n : ~ n > n.
@@ -167,7 +167,7 @@ Notation Zle_or_lt := Z.le_gt_cases (only parsing).
 
 (** Transitivity of strict orders *)
 
-Notation Zlt_trans := Z.lt_trans (compat "8.6").
+Notation Zlt_trans := Z.lt_trans (compat "8.7").
 
 Lemma Zgt_trans n m p : n > m -> m > p -> n > p.
 Proof.
@@ -176,8 +176,8 @@ Qed.
 
 (** Mixed transitivity *)
 
-Notation Zlt_le_trans := Z.lt_le_trans (compat "8.6").
-Notation Zle_lt_trans := Z.le_lt_trans (compat "8.6").
+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.
@@ -191,7 +191,7 @@ Qed.
 
 (** Transitivity of large orders *)
 
-Notation Zle_trans := Z.le_trans (compat "8.6").
+Notation Zle_trans := Z.le_trans (compat "8.7").
 
 Lemma Zge_trans n m p : n >= m -> m >= p -> n >= p.
 Proof.
@@ -257,8 +257,8 @@ Qed.
 
 (** Relating strict and large order using successor or predecessor *)
 
-Notation Zlt_succ_r := Z.lt_succ_r (compat "8.6").
-Notation Zle_succ_l := Z.le_succ_l (compat "8.6").
+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.
@@ -336,8 +336,8 @@ Qed.
 
 (** Special cases of ordered integers *)
 
-Notation Zlt_0_1 := Z.lt_0_1 (compat "8.6").
-Notation Zle_0_1 := Z.le_0_1 (compat "8.6").
+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.
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index a9bc5bd09d..881ead1c4b 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -233,7 +233,7 @@ Qed.
 
 (** * Z.square: a direct definition of [z^2] *)
 
-Notation Psquare := Pos.square (compat "8.6").
-Notation Zsquare := Z.square (compat "8.6").
+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 0c9aca2657..264109dc6f 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -37,17 +37,17 @@ 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.6").
-Notation Zrem_unique := Z.rem_unique (compat "8.6").
-Notation Zrem_1_r := Z.rem_1_r (compat "8.6").
-Notation Zquot_1_r := Z.quot_1_r (compat "8.6").
-Notation Zrem_1_l := Z.rem_1_l (compat "8.6").
-Notation Zquot_1_l := Z.quot_1_l (compat "8.6").
-Notation Z_quot_same := Z.quot_same (compat "8.6").
+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.6").
-Notation Zrem_small := Z.rem_small (compat "8.6").
-Notation Zquot2_quot := Zquot2_quot (compat "8.6").
+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. *)