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

12 files changed, 102 insertions, 102 deletions

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