Notation: a new annotation "compat 8.x" extending "only parsing"

 Suppose we declare : Notation foo := bar (compat "8.3").
 Then each time foo is used in a script :

 - By default nothing particular happens (for the moment)

 - But we could get a warning explaining that
   "foo is bar since coq > 8.3".
   For that, either use the command-line option -verb-compat-notations
   or the interactive command "Set Verbose Compat Notations".

 - There is also a strict mode, where foo is forbidden : the previous
   warning is now an error.
   For that, either use the command-line option -no-compat-notations
   or the interactive command "Unset Compat Notations".

 When Coq is launched in compatibility mode (via -compat 8.x),
 using a notation tagged "8.x" will never trigger a warning or error.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15514 85f007b7-540e-0410-9357-904b9bb8a0f7

17 files changed, 308 insertions, 308 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index f3f7b850e..0f709d686 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1375,87 +1375,87 @@ Infix ">?" := Z.gtb (at level 70, no associativity) : Z_scope.
 
 (** Compatibility Notations *)
 
-Notation Zdouble_plus_one := Z.succ_double (only parsing).
-Notation Zdouble_minus_one := Z.pred_double (only parsing).
-Notation Zdouble := Z.double (only parsing).
-Notation ZPminus := Z.pos_sub (only parsing).
-Notation Zsucc' := Z.succ (only parsing).
-Notation Zpred' := Z.pred (only parsing).
-Notation Zplus' := Z.add (only parsing).
-Notation Zplus := Z.add (only parsing). (* Slightly incompatible *)
-Notation Zopp := Z.opp (only parsing).
-Notation Zsucc := Z.succ (only parsing).
-Notation Zpred := Z.pred (only parsing).
-Notation Zminus := Z.sub (only parsing).
-Notation Zmult := Z.mul (only parsing).
-Notation Zcompare := Z.compare (only parsing).
-Notation Zsgn := Z.sgn (only parsing).
-Notation Zle := Z.le (only parsing).
-Notation Zge := Z.ge (only parsing).
-Notation Zlt := Z.lt (only parsing).
-Notation Zgt := Z.gt (only parsing).
-Notation Zmax := Z.max (only parsing).
-Notation Zmin := Z.min (only parsing).
-Notation Zabs := Z.abs (only parsing).
-Notation Zabs_nat := Z.abs_nat (only parsing).
-Notation Zabs_N := Z.abs_N (only parsing).
-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 (only parsing).
-Notation Zopp_neg := Z.opp_Zneg (only parsing).
-Notation Zopp_involutive := Z.opp_involutive (only parsing).
-Notation Zopp_inj := Z.opp_inj (only parsing).
-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 (only parsing).
-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).
-Notation Zplus_permute := Z.add_shuffle3 (only parsing).
-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 (only parsing).
-Notation Zsucc'_inj := Z.succ_inj (only parsing).
-Notation Zsucc'_pred' := Z.succ_pred (only parsing).
-Notation Zpred'_succ' := Z.pred_succ (only parsing).
-Notation Zpred'_inj := Z.pred_inj (only parsing).
-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).
-Notation Zminus_plus_distr := Z.sub_add_distr (only parsing).
-Notation Zminus_succ_r := Z.sub_succ_r (only parsing).
-Notation Zminus_plus := Z.add_simpl_l (only parsing).
-Notation Zmult_0_l := Z.mul_0_l (only parsing).
-Notation Zmult_0_r := Z.mul_0_r (only parsing).
-Notation Zmult_1_l := Z.mul_1_l (only parsing).
-Notation Zmult_1_r := Z.mul_1_r (only parsing).
-Notation Zmult_comm := Z.mul_comm (only parsing).
-Notation Zmult_assoc := Z.mul_assoc (only parsing).
-Notation Zmult_permute := Z.mul_shuffle3 (only parsing).
-Notation Zmult_1_inversion_l := Z.mul_eq_1 (only parsing).
-Notation Zdouble_mult := Z.double_spec (only parsing).
-Notation Zdouble_plus_one_mult := Z.succ_double_spec (only parsing).
-Notation Zopp_mult_distr_l_reverse := Z.mul_opp_l (only parsing).
-Notation Zmult_opp_opp := Z.mul_opp_opp (only parsing).
-Notation Zmult_opp_comm := Z.mul_opp_comm (only parsing).
-Notation Zopp_eq_mult_neg_1 := Z.opp_eq_mul_m1 (only parsing).
-Notation Zmult_plus_distr_r := Z.mul_add_distr_l (only parsing).
-Notation Zmult_plus_distr_l := Z.mul_add_distr_r (only parsing).
-Notation Zmult_minus_distr_r := Z.mul_sub_distr_r (only parsing).
-Notation Zmult_reg_l := Z.mul_reg_l (only parsing).
-Notation Zmult_reg_r := Z.mul_reg_r (only parsing).
-Notation Zmult_succ_l := Z.mul_succ_l (only parsing).
-Notation Zmult_succ_r := Z.mul_succ_r (only parsing).
-Notation Zpos_xI := Z.pos_xI (only parsing).
-Notation Zpos_xO := Z.pos_xO (only parsing).
-Notation Zneg_xI := Z.neg_xI (only parsing).
-Notation Zneg_xO := Z.neg_xO (only parsing).
+Notation Zdouble_plus_one := Z.succ_double (compat "8.3").
+Notation Zdouble_minus_one := Z.pred_double (compat "8.3").
+Notation Zdouble := Z.double (compat "8.3").
+Notation ZPminus := Z.pos_sub (compat "8.3").
+Notation Zsucc' := Z.succ (compat "8.3").
+Notation Zpred' := Z.pred (compat "8.3").
+Notation Zplus' := Z.add (compat "8.3").
+Notation Zplus := Z.add (compat "8.3"). (* Slightly incompatible *)
+Notation Zopp := Z.opp (compat "8.3").
+Notation Zsucc := Z.succ (compat "8.3").
+Notation Zpred := Z.pred (compat "8.3").
+Notation Zminus := Z.sub (compat "8.3").
+Notation Zmult := Z.mul (compat "8.3").
+Notation Zcompare := Z.compare (compat "8.3").
+Notation Zsgn := Z.sgn (compat "8.3").
+Notation Zle := Z.le (compat "8.3").
+Notation Zge := Z.ge (compat "8.3").
+Notation Zlt := Z.lt (compat "8.3").
+Notation Zgt := Z.gt (compat "8.3").
+Notation Zmax := Z.max (compat "8.3").
+Notation Zmin := Z.min (compat "8.3").
+Notation Zabs := Z.abs (compat "8.3").
+Notation Zabs_nat := Z.abs_nat (compat "8.3").
+Notation Zabs_N := Z.abs_N (compat "8.3").
+Notation Z_of_nat := Z.of_nat (compat "8.3").
+Notation Z_of_N := Z.of_N (compat "8.3").
+
+Notation Zind := Z.peano_ind (compat "8.3").
+Notation Zopp_0 := Z.opp_0 (compat "8.3").
+Notation Zopp_neg := Z.opp_Zneg (compat "8.3").
+Notation Zopp_involutive := Z.opp_involutive (compat "8.3").
+Notation Zopp_inj := Z.opp_inj (compat "8.3").
+Notation Zplus_0_l := Z.add_0_l (compat "8.3").
+Notation Zplus_0_r := Z.add_0_r (compat "8.3").
+Notation Zplus_comm := Z.add_comm (compat "8.3").
+Notation Zopp_plus_distr := Z.opp_add_distr (compat "8.3").
+Notation Zopp_succ := Z.opp_succ (compat "8.3").
+Notation Zplus_opp_r := Z.add_opp_diag_r (compat "8.3").
+Notation Zplus_opp_l := Z.add_opp_diag_l (compat "8.3").
+Notation Zplus_assoc := Z.add_assoc (compat "8.3").
+Notation Zplus_permute := Z.add_shuffle3 (compat "8.3").
+Notation Zplus_reg_l := Z.add_reg_l (compat "8.3").
+Notation Zplus_succ_l := Z.add_succ_l (compat "8.3").
+Notation Zplus_succ_comm := Z.add_succ_comm (compat "8.3").
+Notation Zsucc_discr := Z.neq_succ_diag_r (compat "8.3").
+Notation Zsucc_inj := Z.succ_inj (compat "8.3").
+Notation Zsucc'_inj := Z.succ_inj (compat "8.3").
+Notation Zsucc'_pred' := Z.succ_pred (compat "8.3").
+Notation Zpred'_succ' := Z.pred_succ (compat "8.3").
+Notation Zpred'_inj := Z.pred_inj (compat "8.3").
+Notation Zsucc'_discr := Z.neq_succ_diag_r (compat "8.3").
+Notation Zminus_0_r := Z.sub_0_r (compat "8.3").
+Notation Zminus_diag := Z.sub_diag (compat "8.3").
+Notation Zminus_plus_distr := Z.sub_add_distr (compat "8.3").
+Notation Zminus_succ_r := Z.sub_succ_r (compat "8.3").
+Notation Zminus_plus := Z.add_simpl_l (compat "8.3").
+Notation Zmult_0_l := Z.mul_0_l (compat "8.3").
+Notation Zmult_0_r := Z.mul_0_r (compat "8.3").
+Notation Zmult_1_l := Z.mul_1_l (compat "8.3").
+Notation Zmult_1_r := Z.mul_1_r (compat "8.3").
+Notation Zmult_comm := Z.mul_comm (compat "8.3").
+Notation Zmult_assoc := Z.mul_assoc (compat "8.3").
+Notation Zmult_permute := Z.mul_shuffle3 (compat "8.3").
+Notation Zmult_1_inversion_l := Z.mul_eq_1 (compat "8.3").
+Notation Zdouble_mult := Z.double_spec (compat "8.3").
+Notation Zdouble_plus_one_mult := Z.succ_double_spec (compat "8.3").
+Notation Zopp_mult_distr_l_reverse := Z.mul_opp_l (compat "8.3").
+Notation Zmult_opp_opp := Z.mul_opp_opp (compat "8.3").
+Notation Zmult_opp_comm := Z.mul_opp_comm (compat "8.3").
+Notation Zopp_eq_mult_neg_1 := Z.opp_eq_mul_m1 (compat "8.3").
+Notation Zmult_plus_distr_r := Z.mul_add_distr_l (compat "8.3").
+Notation Zmult_plus_distr_l := Z.mul_add_distr_r (compat "8.3").
+Notation Zmult_minus_distr_r := Z.mul_sub_distr_r (compat "8.3").
+Notation Zmult_reg_l := Z.mul_reg_l (compat "8.3").
+Notation Zmult_reg_r := Z.mul_reg_r (compat "8.3").
+Notation Zmult_succ_l := Z.mul_succ_l (compat "8.3").
+Notation Zmult_succ_r := Z.mul_succ_r (compat "8.3").
+Notation Zpos_xI := Z.pos_xI (compat "8.3").
+Notation Zpos_xO := Z.pos_xO (compat "8.3").
+Notation Zneg_xI := Z.neg_xI (compat "8.3").
+Notation Zneg_xO := Z.neg_xO (compat "8.3").
 
 Notation Z := Z (only parsing).
 Notation Z_rect := Z_rect (only parsing).
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index 76308e60b..ca26787bd 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -36,7 +36,7 @@ Proof.
   intro; apply Zcompare_rect.
 Defined.
 
-Notation Z_eq_dec := Z.eq_dec (only parsing).
+Notation Z_eq_dec := Z.eq_dec (compat "8.3").
 
 Section decidability.
 
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index 23473e932..2e43b3554 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -27,17 +27,17 @@ Local Open Scope Z_scope.
 (**********************************************************************)
 (** * Properties of absolute value *)
 
-Notation Zabs_eq := Z.abs_eq (only parsing).
-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 (only parsing).
-Notation Zabs_eq_case := Z.abs_eq_cases (only parsing).
-Notation Zabs_triangle := Z.abs_triangle (only parsing).
-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 (only parsing).
+Notation Zabs_eq := Z.abs_eq (compat "8.3").
+Notation Zabs_non_eq := Z.abs_neq (compat "8.3").
+Notation Zabs_Zopp := Z.abs_opp (compat "8.3").
+Notation Zabs_pos := Z.abs_nonneg (compat "8.3").
+Notation Zabs_involutive := Z.abs_involutive (compat "8.3").
+Notation Zabs_eq_case := Z.abs_eq_cases (compat "8.3").
+Notation Zabs_triangle := Z.abs_triangle (compat "8.3").
+Notation Zsgn_Zabs := Z.sgn_abs (compat "8.3").
+Notation Zabs_Zsgn := Z.abs_sgn (compat "8.3").
+Notation Zabs_Zmult := Z.abs_mul (compat "8.3").
+Notation Zabs_square := Z.abs_square (compat "8.3").
 
 (** * Proving a property of the absolute value by cases *)
 
@@ -68,11 +68,11 @@ Qed.
 
 (** * Some results about the sign function. *)
 
-Notation Zsgn_Zmult := Z.sgn_mul (only parsing).
-Notation Zsgn_Zopp := Z.sgn_opp (only parsing).
-Notation Zsgn_pos := Z.sgn_pos_iff (only parsing).
-Notation Zsgn_neg := Z.sgn_neg_iff (only parsing).
-Notation Zsgn_null := Z.sgn_null_iff (only parsing).
+Notation Zsgn_Zmult := Z.sgn_mul (compat "8.3").
+Notation Zsgn_Zopp := Z.sgn_opp (compat "8.3").
+Notation Zsgn_pos := Z.sgn_pos_iff (compat "8.3").
+Notation Zsgn_neg := Z.sgn_neg_iff (compat "8.3").
+Notation Zsgn_null := Z.sgn_null_iff (compat "8.3").
 
 (** A characterization of the sign function: *)
 
@@ -86,13 +86,13 @@ Qed.
 
 (** Compatibility *)
 
-Notation inj_Zabs_nat := Zabs2Nat.id_abs (only parsing).
-Notation Zabs_nat_Z_of_nat := Zabs2Nat.id (only parsing).
-Notation Zabs_nat_mult := Zabs2Nat.inj_mul (only parsing).
-Notation Zabs_nat_Zsucc := Zabs2Nat.inj_succ (only parsing).
-Notation Zabs_nat_Zplus := Zabs2Nat.inj_add (only parsing).
-Notation Zabs_nat_Zminus := (fun n m => Zabs2Nat.inj_sub m n) (only parsing).
-Notation Zabs_nat_compare := Zabs2Nat.inj_compare (only parsing).
+Notation inj_Zabs_nat := Zabs2Nat.id_abs (compat "8.3").
+Notation Zabs_nat_Z_of_nat := Zabs2Nat.id (compat "8.3").
+Notation Zabs_nat_mult := Zabs2Nat.inj_mul (compat "8.3").
+Notation Zabs_nat_Zsucc := Zabs2Nat.inj_succ (compat "8.3").
+Notation Zabs_nat_Zplus := Zabs2Nat.inj_add (compat "8.3").
+Notation Zabs_nat_Zminus := (fun n m => Zabs2Nat.inj_sub m n) (compat "8.3").
+Notation Zabs_nat_compare := Zabs2Nat.inj_compare (compat "8.3").
 
 Lemma Zabs_nat_le n m : 0 <= n <= m -> (Z.abs_nat n <= Z.abs_nat m)%nat.
 Proof.
diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v
index d09012820..7c1e096ed 100644
--- a/theories/ZArith/Zbool.v
+++ b/theories/ZArith/Zbool.v
@@ -33,10 +33,10 @@ Definition Zeven_odd_bool (x:Z) := bool_of_sumbool (Zeven_odd_dec x).
 (**********************************************************************)
 (** * Boolean comparisons of binary integers *)
 
-Notation Zle_bool := Z.leb (only parsing).
-Notation Zge_bool := Z.geb (only parsing).
-Notation Zlt_bool := Z.ltb (only parsing).
-Notation Zgt_bool := Z.gtb (only parsing).
+Notation Zle_bool := Z.leb (compat "8.3").
+Notation Zge_bool := Z.geb (compat "8.3").
+Notation Zlt_bool := Z.ltb (compat "8.3").
+Notation Zgt_bool := Z.gtb (compat "8.3").
 
 (** We now provide a direct [Z.eqb] that doesn't refer to [Z.compare].
    The old [Zeq_bool] is kept for compatibility. *)
@@ -87,7 +87,7 @@ Proof.
  apply Z.leb_le.
 Qed.
 
-Notation Zle_bool_refl := Z.leb_refl (only parsing).
+Notation Zle_bool_refl := Z.leb_refl (compat "8.3").
 
 Lemma Zle_bool_antisym n m :
  (n <=? m) = true -> (m <=? n) = true -> n = m.
diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v
index 20e1b006a..703a3972f 100644
--- a/theories/ZArith/Zcompare.v
+++ b/theories/ZArith/Zcompare.v
@@ -181,18 +181,18 @@ Qed.
 
 (** Compatibility notations *)
 
-Notation Zcompare_refl := Z.compare_refl (only parsing).
-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 (only parsing).
-Notation Zmin_l := Z.min_l (only parsing).
-Notation Zmin_r := Z.min_r (only parsing).
-Notation Zmax_l := Z.max_l (only parsing).
-Notation Zmax_r := Z.max_r (only parsing).
-Notation Zabs_eq := Z.abs_eq (only parsing).
-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).
-Notation Zsgn_m1 := Z.sgn_neg (only parsing).
+Notation Zcompare_refl := Z.compare_refl (compat "8.3").
+Notation Zcompare_Eq_eq := Z.compare_eq (compat "8.3").
+Notation Zcompare_Eq_iff_eq := Z.compare_eq_iff (compat "8.3").
+Notation Zcompare_spec := Z.compare_spec (compat "8.3").
+Notation Zmin_l := Z.min_l (compat "8.3").
+Notation Zmin_r := Z.min_r (compat "8.3").
+Notation Zmax_l := Z.max_l (compat "8.3").
+Notation Zmax_r := Z.max_r (compat "8.3").
+Notation Zabs_eq := Z.abs_eq (compat "8.3").
+Notation Zabs_non_eq := Z.abs_neq (compat "8.3").
+Notation Zsgn_0 := Z.sgn_null (compat "8.3").
+Notation Zsgn_1 := Z.sgn_pos (compat "8.3").
+Notation Zsgn_m1 := Z.sgn_neg (compat "8.3").
 
 (** Not kept: Zcompare_egal_dec *)
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 314f696a2..057fd6d34 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -18,16 +18,16 @@ Local Open Scope Z_scope.
 (** The definition of the division is now in [BinIntDef], the initial
     specifications and properties are in [BinInt]. *)
 
-Notation Zdiv_eucl_POS := Z.pos_div_eucl (only parsing).
-Notation Zdiv_eucl := Z.div_eucl (only parsing).
-Notation Zdiv := Z.div (only parsing).
-Notation Zmod := Z.modulo (only parsing).
-
-Notation Zdiv_eucl_eq := Z.div_eucl_eq (only parsing).
-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).
-Notation Zmod_neg_bound := Z.mod_neg_bound (only parsing).
+Notation Zdiv_eucl_POS := Z.pos_div_eucl (compat "8.3").
+Notation Zdiv_eucl := Z.div_eucl (compat "8.3").
+Notation Zdiv := Z.div (compat "8.3").
+Notation Zmod := Z.modulo (compat "8.3").
+
+Notation Zdiv_eucl_eq := Z.div_eucl_eq (compat "8.3").
+Notation Z_div_mod_eq_full := Z.div_mod (compat "8.3").
+Notation Zmod_POS_bound := Z.pos_div_eucl_bound (compat "8.3").
+Notation Zmod_pos_bound := Z.mod_pos_bound (compat "8.3").
+Notation Zmod_neg_bound := Z.mod_neg_bound (compat "8.3").
 
 (** * Main division theorems *)
 
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index 8e6cc07bf..a032a801d 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -58,8 +58,8 @@ Proof (Zodd_equiv n).
 
 (** Boolean tests of parity (now in BinInt.Z) *)
 
-Notation Zeven_bool := Z.even (only parsing).
-Notation Zodd_bool := Z.odd (only parsing).
+Notation Zeven_bool := Z.even (compat "8.3").
+Notation Zodd_bool := Z.odd (compat "8.3").
 
 Lemma Zeven_bool_iff n : Z.even n = true <-> Zeven n.
 Proof.
@@ -130,17 +130,17 @@ Qed.
 
 Hint Unfold Zeven Zodd: zarith.
 
-Notation Zeven_bool_succ := Z.even_succ (only parsing).
-Notation Zeven_bool_pred := Z.even_pred (only parsing).
-Notation Zodd_bool_succ := Z.odd_succ (only parsing).
-Notation Zodd_bool_pred := Z.odd_pred (only parsing).
+Notation Zeven_bool_succ := Z.even_succ (compat "8.3").
+Notation Zeven_bool_pred := Z.even_pred (compat "8.3").
+Notation Zodd_bool_succ := Z.odd_succ (compat "8.3").
+Notation Zodd_bool_pred := Z.odd_pred (compat "8.3").
 
 (******************************************************************)
 (** * Definition of [Zquot2], [Zdiv2] and properties wrt [Zeven]
   and [Zodd] *)
 
-Notation Zdiv2 := Z.div2 (only parsing).
-Notation Zquot2 := Z.quot2 (only parsing).
+Notation Zdiv2 := Z.div2 (compat "8.3").
+Notation Zquot2 := Z.quot2 (compat "8.3").
 
 (** Properties of [Z.div2] *)
 
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index 999564f03..a3eeb4160 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -104,8 +104,8 @@ Qed.
 
 (* begin hide *)
 (* Compatibility *)
-Notation Zmax1 := Z.le_max_l (only parsing).
-Notation Zmax2 := Z.le_max_r (only parsing).
-Notation Zmax_irreducible_inf := Z.max_dec (only parsing).
-Notation Zmax_le_prime_inf := Z.max_le (only parsing).
+Notation Zmax1 := Z.le_max_l (compat "8.3").
+Notation Zmax2 := Z.le_max_r (compat "8.3").
+Notation Zmax_irreducible_inf := Z.max_dec (compat "8.3").
+Notation Zmax_le_prime_inf := Z.max_le (compat "8.3").
 (* end hide *)
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index 2c5003a6d..fbb31632c 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -45,7 +45,7 @@ Proof Z.min_le_compat_l.
 (** * Semi-lattice properties of min *)
 
 Lemma Zmin_idempotent : forall n, Z.min n n = n. Proof Z.min_id.
-Notation Zmin_n_n := Z.min_id (only parsing).
+Notation Zmin_n_n := Z.min_id (compat "8.3").
 Lemma Zmin_comm : forall n m, Z.min n m = Z.min m n. Proof Z.min_comm.
 Lemma Zmin_assoc : forall n m p, Z.min n (Z.min m p) = Z.min (Z.min n m) p.
 Proof Z.min_assoc.
diff --git a/theories/ZArith/Zminmax.v b/theories/ZArith/Zminmax.v
index 8908175f6..8c22efc30 100644
--- a/theories/ZArith/Zminmax.v
+++ b/theories/ZArith/Zminmax.v
@@ -12,11 +12,11 @@ Require Import Orders BinInt Zcompare Zorder.
 
 (*begin hide*)
 (* Compatibility with names of the old Zminmax file *)
-Notation Zmin_max_absorption_r_r := Z.min_max_absorption (only parsing).
-Notation Zmax_min_absorption_r_r := Z.max_min_absorption (only parsing).
-Notation Zmax_min_distr_r := Z.max_min_distr (only parsing).
-Notation Zmin_max_distr_r := Z.min_max_distr (only parsing).
-Notation Zmax_min_modular_r := Z.max_min_modular (only parsing).
-Notation Zmin_max_modular_r := Z.min_max_modular (only parsing).
-Notation max_min_disassoc := Z.max_min_disassoc (only parsing).
+Notation Zmin_max_absorption_r_r := Z.min_max_absorption (compat "8.3").
+Notation Zmax_min_absorption_r_r := Z.max_min_absorption (compat "8.3").
+Notation Zmax_min_distr_r := Z.max_min_distr (compat "8.3").
+Notation Zmin_max_distr_r := Z.min_max_distr (compat "8.3").
+Notation Zmax_min_modular_r := Z.max_min_modular (compat "8.3").
+Notation Zmin_max_modular_r := Z.min_max_modular (compat "8.3").
+Notation max_min_disassoc := Z.max_min_disassoc (compat "8.3").
 (*end hide*)
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index ff844ec28..a6da9d7e7 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -18,7 +18,7 @@ Open Local Scope Z_scope.
 
 (** [n]th iteration of the function [f] *)
 
-Notation iter := @Z.iter (only parsing).
+Notation iter := @Z.iter (compat "8.3").
 
 Lemma iter_nat_of_Z : forall n A f x, 0 <= n ->
   iter n A f x = iter_nat (Z.abs_nat n) A f x.
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index e3843990c..2c3288f6c 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -931,65 +931,65 @@ Definition inj_gt n m := proj1 (Nat2Z.inj_gt n m).
 
 (** For the others, a Notation is fine *)
 
-Notation inj_0 := Nat2Z.inj_0 (only parsing).
-Notation inj_S := Nat2Z.inj_succ (only parsing).
-Notation inj_compare := Nat2Z.inj_compare (only parsing).
-Notation inj_eq_rev := Nat2Z.inj (only parsing).
-Notation inj_eq_iff := (fun n m => iff_sym (Nat2Z.inj_iff n m)) (only parsing).
-Notation inj_le_iff := Nat2Z.inj_le (only parsing).
-Notation inj_lt_iff := Nat2Z.inj_lt (only parsing).
-Notation inj_ge_iff := Nat2Z.inj_ge (only parsing).
-Notation inj_gt_iff := Nat2Z.inj_gt (only parsing).
-Notation inj_le_rev := (fun n m => proj2 (Nat2Z.inj_le n m)) (only parsing).
-Notation inj_lt_rev := (fun n m => proj2 (Nat2Z.inj_lt n m)) (only parsing).
-Notation inj_ge_rev := (fun n m => proj2 (Nat2Z.inj_ge n m)) (only parsing).
-Notation inj_gt_rev := (fun n m => proj2 (Nat2Z.inj_gt n m)) (only parsing).
-Notation inj_plus := Nat2Z.inj_add (only parsing).
-Notation inj_mult := Nat2Z.inj_mul (only parsing).
-Notation inj_minus1 := Nat2Z.inj_sub (only parsing).
-Notation inj_minus := Nat2Z.inj_sub_max (only parsing).
-Notation inj_min := Nat2Z.inj_min (only parsing).
-Notation inj_max := Nat2Z.inj_max (only parsing).
-
-Notation Z_of_nat_of_P := positive_nat_Z (only parsing).
+Notation inj_0 := Nat2Z.inj_0 (compat "8.3").
+Notation inj_S := Nat2Z.inj_succ (compat "8.3").
+Notation inj_compare := Nat2Z.inj_compare (compat "8.3").
+Notation inj_eq_rev := Nat2Z.inj (compat "8.3").
+Notation inj_eq_iff := (fun n m => iff_sym (Nat2Z.inj_iff n m)) (compat "8.3").
+Notation inj_le_iff := Nat2Z.inj_le (compat "8.3").
+Notation inj_lt_iff := Nat2Z.inj_lt (compat "8.3").
+Notation inj_ge_iff := Nat2Z.inj_ge (compat "8.3").
+Notation inj_gt_iff := Nat2Z.inj_gt (compat "8.3").
+Notation inj_le_rev := (fun n m => proj2 (Nat2Z.inj_le n m)) (compat "8.3").
+Notation inj_lt_rev := (fun n m => proj2 (Nat2Z.inj_lt n m)) (compat "8.3").
+Notation inj_ge_rev := (fun n m => proj2 (Nat2Z.inj_ge n m)) (compat "8.3").
+Notation inj_gt_rev := (fun n m => proj2 (Nat2Z.inj_gt n m)) (compat "8.3").
+Notation inj_plus := Nat2Z.inj_add (compat "8.3").
+Notation inj_mult := Nat2Z.inj_mul (compat "8.3").
+Notation inj_minus1 := Nat2Z.inj_sub (compat "8.3").
+Notation inj_minus := Nat2Z.inj_sub_max (compat "8.3").
+Notation inj_min := Nat2Z.inj_min (compat "8.3").
+Notation inj_max := Nat2Z.inj_max (compat "8.3").
+
+Notation Z_of_nat_of_P := positive_nat_Z (compat "8.3").
 Notation Zpos_eq_Z_of_nat_o_nat_of_P :=
-  (fun p => sym_eq (positive_nat_Z p)) (only parsing).
-
-Notation Z_of_nat_of_N := N_nat_Z (only parsing).
-Notation Z_of_N_of_nat := nat_N_Z (only parsing).
-
-Notation Z_of_N_eq := (f_equal Z.of_N) (only parsing).
-Notation Z_of_N_eq_rev := N2Z.inj (only parsing).
-Notation Z_of_N_eq_iff := (fun n m => iff_sym (N2Z.inj_iff n m)) (only parsing).
-Notation Z_of_N_compare := N2Z.inj_compare (only parsing).
-Notation Z_of_N_le_iff := N2Z.inj_le (only parsing).
-Notation Z_of_N_lt_iff := N2Z.inj_lt (only parsing).
-Notation Z_of_N_ge_iff := N2Z.inj_ge (only parsing).
-Notation Z_of_N_gt_iff := N2Z.inj_gt (only parsing).
-Notation Z_of_N_le := (fun n m => proj1 (N2Z.inj_le n m)) (only parsing).
-Notation Z_of_N_lt := (fun n m => proj1 (N2Z.inj_lt n m)) (only parsing).
-Notation Z_of_N_ge := (fun n m => proj1 (N2Z.inj_ge n m)) (only parsing).
-Notation Z_of_N_gt := (fun n m => proj1 (N2Z.inj_gt n m)) (only parsing).
-Notation Z_of_N_le_rev := (fun n m => proj2 (N2Z.inj_le n m)) (only parsing).
-Notation Z_of_N_lt_rev := (fun n m => proj2 (N2Z.inj_lt n m)) (only parsing).
-Notation Z_of_N_ge_rev := (fun n m => proj2 (N2Z.inj_ge n m)) (only parsing).
-Notation Z_of_N_gt_rev := (fun n m => proj2 (N2Z.inj_gt n m)) (only parsing).
-Notation Z_of_N_pos := N2Z.inj_pos (only parsing).
-Notation Z_of_N_abs := N2Z.inj_abs_N (only parsing).
-Notation Z_of_N_le_0 := N2Z.is_nonneg (only parsing).
-Notation Z_of_N_plus := N2Z.inj_add (only parsing).
-Notation Z_of_N_mult := N2Z.inj_mul (only parsing).
-Notation Z_of_N_minus := N2Z.inj_sub_max (only parsing).
-Notation Z_of_N_succ := N2Z.inj_succ (only parsing).
-Notation Z_of_N_min := N2Z.inj_min (only parsing).
-Notation Z_of_N_max := N2Z.inj_max (only parsing).
-Notation Zabs_of_N := Zabs2N.id (only parsing).
-Notation Zabs_N_succ_abs := Zabs2N.inj_succ_abs (only parsing).
-Notation Zabs_N_succ := Zabs2N.inj_succ (only parsing).
-Notation Zabs_N_plus_abs := Zabs2N.inj_add_abs (only parsing).
-Notation Zabs_N_plus := Zabs2N.inj_add (only parsing).
-Notation Zabs_N_mult_abs := Zabs2N.inj_mul_abs (only parsing).
-Notation Zabs_N_mult := Zabs2N.inj_mul (only parsing).
+  (fun p => sym_eq (positive_nat_Z p)) (compat "8.3").
+
+Notation Z_of_nat_of_N := N_nat_Z (compat "8.3").
+Notation Z_of_N_of_nat := nat_N_Z (compat "8.3").
+
+Notation Z_of_N_eq := (f_equal Z.of_N) (compat "8.3").
+Notation Z_of_N_eq_rev := N2Z.inj (compat "8.3").
+Notation Z_of_N_eq_iff := (fun n m => iff_sym (N2Z.inj_iff n m)) (compat "8.3").
+Notation Z_of_N_compare := N2Z.inj_compare (compat "8.3").
+Notation Z_of_N_le_iff := N2Z.inj_le (compat "8.3").
+Notation Z_of_N_lt_iff := N2Z.inj_lt (compat "8.3").
+Notation Z_of_N_ge_iff := N2Z.inj_ge (compat "8.3").
+Notation Z_of_N_gt_iff := N2Z.inj_gt (compat "8.3").
+Notation Z_of_N_le := (fun n m => proj1 (N2Z.inj_le n m)) (compat "8.3").
+Notation Z_of_N_lt := (fun n m => proj1 (N2Z.inj_lt n m)) (compat "8.3").
+Notation Z_of_N_ge := (fun n m => proj1 (N2Z.inj_ge n m)) (compat "8.3").
+Notation Z_of_N_gt := (fun n m => proj1 (N2Z.inj_gt n m)) (compat "8.3").
+Notation Z_of_N_le_rev := (fun n m => proj2 (N2Z.inj_le n m)) (compat "8.3").
+Notation Z_of_N_lt_rev := (fun n m => proj2 (N2Z.inj_lt n m)) (compat "8.3").
+Notation Z_of_N_ge_rev := (fun n m => proj2 (N2Z.inj_ge n m)) (compat "8.3").
+Notation Z_of_N_gt_rev := (fun n m => proj2 (N2Z.inj_gt n m)) (compat "8.3").
+Notation Z_of_N_pos := N2Z.inj_pos (compat "8.3").
+Notation Z_of_N_abs := N2Z.inj_abs_N (compat "8.3").
+Notation Z_of_N_le_0 := N2Z.is_nonneg (compat "8.3").
+Notation Z_of_N_plus := N2Z.inj_add (compat "8.3").
+Notation Z_of_N_mult := N2Z.inj_mul (compat "8.3").
+Notation Z_of_N_minus := N2Z.inj_sub_max (compat "8.3").
+Notation Z_of_N_succ := N2Z.inj_succ (compat "8.3").
+Notation Z_of_N_min := N2Z.inj_min (compat "8.3").
+Notation Z_of_N_max := N2Z.inj_max (compat "8.3").
+Notation Zabs_of_N := Zabs2N.id (compat "8.3").
+Notation Zabs_N_succ_abs := Zabs2N.inj_succ_abs (compat "8.3").
+Notation Zabs_N_succ := Zabs2N.inj_succ (compat "8.3").
+Notation Zabs_N_plus_abs := Zabs2N.inj_add_abs (compat "8.3").
+Notation Zabs_N_plus := Zabs2N.inj_add (compat "8.3").
+Notation Zabs_N_mult_abs := Zabs2N.inj_mul_abs (compat "8.3").
+Notation Zabs_N_mult := Zabs2N.inj_mul (compat "8.3").
 
 Theorem inj_minus2 : forall n m:nat, (m > n)%nat -> Z_of_nat (n - m) = 0.
 Proof.
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 814b67322..00019b1a3 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -25,20 +25,20 @@ Open Scope Z_scope.
      - properties of the efficient [Z.gcd] function
 *)
 
-Notation Zgcd := Z.gcd (only parsing).
-Notation Zggcd := Z.ggcd (only parsing).
-Notation Zggcd_gcd := Z.ggcd_gcd (only parsing).
-Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (only parsing).
-Notation Zgcd_divide_l := Z.gcd_divide_l (only parsing).
-Notation Zgcd_divide_r := Z.gcd_divide_r (only parsing).
-Notation Zgcd_greatest := Z.gcd_greatest (only parsing).
-Notation Zgcd_nonneg := Z.gcd_nonneg (only parsing).
-Notation Zggcd_opp := Z.ggcd_opp (only parsing).
+Notation Zgcd := Z.gcd (compat "8.3").
+Notation Zggcd := Z.ggcd (compat "8.3").
+Notation Zggcd_gcd := Z.ggcd_gcd (compat "8.3").
+Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (compat "8.3").
+Notation Zgcd_divide_l := Z.gcd_divide_l (compat "8.3").
+Notation Zgcd_divide_r := Z.gcd_divide_r (compat "8.3").
+Notation Zgcd_greatest := Z.gcd_greatest (compat "8.3").
+Notation Zgcd_nonneg := Z.gcd_nonneg (compat "8.3").
+Notation Zggcd_opp := Z.ggcd_opp (compat "8.3").
 
 (** The former specialized inductive predicate [Zdivide] is now
     a generic existential predicate. *)
 
-Notation Zdivide := Z.divide (only parsing).
+Notation Zdivide := Z.divide (compat "8.3").
 
 (** Its former constructor is now a pseudo-constructor. *)
 
@@ -46,17 +46,17 @@ 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 (only parsing).
-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).
-Notation Zmult_divide_compat_r := Z.mul_divide_mono_r (only parsing).
-Notation Zdivide_plus_r := Z.divide_add_r (only parsing).
-Notation Zdivide_minus_l := Z.divide_sub_r (only parsing).
-Notation Zdivide_mult_l := Z.divide_mul_l (only parsing).
-Notation Zdivide_mult_r := Z.divide_mul_r (only parsing).
-Notation Zdivide_factor_r := Z.divide_factor_l (only parsing).
-Notation Zdivide_factor_l := Z.divide_factor_r (only parsing).
+Notation Zdivide_refl := Z.divide_refl (compat "8.3").
+Notation Zone_divide := Z.divide_1_l (compat "8.3").
+Notation Zdivide_0 := Z.divide_0_r (compat "8.3").
+Notation Zmult_divide_compat_l := Z.mul_divide_mono_l (compat "8.3").
+Notation Zmult_divide_compat_r := Z.mul_divide_mono_r (compat "8.3").
+Notation Zdivide_plus_r := Z.divide_add_r (compat "8.3").
+Notation Zdivide_minus_l := Z.divide_sub_r (compat "8.3").
+Notation Zdivide_mult_l := Z.divide_mul_l (compat "8.3").
+Notation Zdivide_mult_r := Z.divide_mul_r (compat "8.3").
+Notation Zdivide_factor_r := Z.divide_factor_l (compat "8.3").
+Notation Zdivide_factor_l := Z.divide_factor_r (compat "8.3").
 
 Lemma Zdivide_opp_r a b : (a | b) -> (a | - b).
 Proof. apply Z.divide_opp_r. Qed.
@@ -91,12 +91,12 @@ Qed.
 
 (** Only [1] and [-1] divide [1]. *)
 
-Notation Zdivide_1 := Z.divide_1_r (only parsing).
+Notation Zdivide_1 := Z.divide_1_r (compat "8.3").
 
 (** If [a] divides [b] and [b] divides [a] then [a] is [b] or [-b]. *)
 
-Notation Zdivide_antisym := Z.divide_antisym (only parsing).
-Notation Zdivide_trans := Z.divide_trans (only parsing).
+Notation Zdivide_antisym := Z.divide_antisym (compat "8.3").
+Notation Zdivide_trans := Z.divide_trans (compat "8.3").
 
 (** If [a] divides [b] and [b<>0] then [|a| <= |b|]. *)
 
@@ -742,7 +742,7 @@ Qed.
 (** we now prove that [Z.gcd] is indeed a gcd in
    the sense of [Zis_gcd]. *)
 
-Notation Zgcd_is_pos := Z.gcd_nonneg (only parsing).
+Notation Zgcd_is_pos := Z.gcd_nonneg (compat "8.3").
 
 Lemma Zgcd_is_gcd : forall a b, Zis_gcd a b (Z.gcd a b).
 Proof.
@@ -775,8 +775,8 @@ Proof.
   subst. now case (Z.gcd a b).
 Qed.
 
-Notation Zgcd_inv_0_l := Z.gcd_eq_0_l (only parsing).
-Notation Zgcd_inv_0_r := Z.gcd_eq_0_r (only parsing).
+Notation Zgcd_inv_0_l := Z.gcd_eq_0_l (compat "8.3").
+Notation Zgcd_inv_0_r := Z.gcd_eq_0_r (compat "8.3").
 
 Theorem Zgcd_div_swap0 : forall a b : Z,
  0 < Z.gcd a b ->
@@ -806,16 +806,16 @@ Proof.
   rewrite <- Zdivide_Zdiv_eq; auto.
 Qed.
 
-Notation Zgcd_comm := Z.gcd_comm (only parsing).
+Notation Zgcd_comm := Z.gcd_comm (compat "8.3").
 
 Lemma Zgcd_ass a b c : Zgcd (Zgcd a b) c = Zgcd a (Zgcd b c).
 Proof.
  symmetry. apply Z.gcd_assoc.
 Qed.
 
-Notation Zgcd_Zabs := Z.gcd_abs_l (only parsing).
-Notation Zgcd_0 := Z.gcd_0_r (only parsing).
-Notation Zgcd_1 := Z.gcd_1_r (only parsing).
+Notation Zgcd_Zabs := Z.gcd_abs_l (compat "8.3").
+Notation Zgcd_0 := Z.gcd_0_r (compat "8.3").
+Notation Zgcd_1 := Z.gcd_1_r (compat "8.3").
 
 Hint Resolve Zgcd_0 Zgcd_1 : zarith.
 
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index a8cd69bb3..d22e2d57c 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -38,9 +38,9 @@ Qed.
 (**********************************************************************)
 (** * Decidability of equality and order on Z *)
 
-Notation dec_eq := Z.eq_decidable (only parsing).
-Notation dec_Zle := Z.le_decidable (only parsing).
-Notation dec_Zlt := Z.lt_decidable (only parsing).
+Notation dec_eq := Z.eq_decidable (compat "8.3").
+Notation dec_Zle := Z.le_decidable (compat "8.3").
+Notation dec_Zlt := Z.lt_decidable (compat "8.3").
 
 Theorem dec_Zne n m : decidable (Zne n m).
 Proof.
@@ -64,12 +64,12 @@ Qed.
 
 (** * Relating strict and large orders *)
 
-Notation Zgt_lt := Z.gt_lt (only parsing).
-Notation Zlt_gt := Z.lt_gt (only parsing).
-Notation Zge_le := Z.ge_le (only parsing).
-Notation Zle_ge := Z.le_ge (only parsing).
-Notation Zgt_iff_lt := Z.gt_lt_iff (only parsing).
-Notation Zge_iff_le := Z.ge_le_iff (only parsing).
+Notation Zgt_lt := Z.gt_lt (compat "8.3").
+Notation Zlt_gt := Z.lt_gt (compat "8.3").
+Notation Zge_le := Z.ge_le (compat "8.3").
+Notation Zle_ge := Z.le_ge (compat "8.3").
+Notation Zgt_iff_lt := Z.gt_lt_iff (compat "8.3").
+Notation Zge_iff_le := Z.ge_le_iff (compat "8.3").
 
 Lemma Zle_not_lt n m : n <= m -> ~ m < n.
 Proof.
@@ -121,18 +121,18 @@ Qed.
 
 (** Reflexivity *)
 
-Notation Zle_refl := Z.le_refl (only parsing).
-Notation Zeq_le := Z.eq_le_incl (only parsing).
+Notation Zle_refl := Z.le_refl (compat "8.3").
+Notation Zeq_le := Z.eq_le_incl (compat "8.3").
 
 Hint Resolve Z.le_refl: zarith.
 
 (** Antisymmetry *)
 
-Notation Zle_antisym := Z.le_antisymm (only parsing).
+Notation Zle_antisym := Z.le_antisymm (compat "8.3").
 
 (** Asymmetry *)
 
-Notation Zlt_asym := Z.lt_asymm (only parsing).
+Notation Zlt_asym := Z.lt_asymm (compat "8.3").
 
 Lemma Zgt_asym n m : n > m -> ~ m > n.
 Proof.
@@ -141,8 +141,8 @@ Qed.
 
 (** Irreflexivity *)
 
-Notation Zlt_irrefl := Z.lt_irrefl (only parsing).
-Notation Zlt_not_eq := Z.lt_neq (only parsing).
+Notation Zlt_irrefl := Z.lt_irrefl (compat "8.3").
+Notation Zlt_not_eq := Z.lt_neq (compat "8.3").
 
 Lemma Zgt_irrefl n : ~ n > n.
 Proof.
@@ -151,8 +151,8 @@ Qed.
 
 (** Large = strict or equal *)
 
-Notation Zlt_le_weak := Z.lt_le_incl (only parsing).
-Notation Zle_lt_or_eq_iff := Z.lt_eq_cases (only parsing).
+Notation Zlt_le_weak := Z.lt_le_incl (compat "8.3").
+Notation Zle_lt_or_eq_iff := Z.lt_eq_cases (compat "8.3").
 
 Lemma Zle_lt_or_eq n m : n <= m -> n < m \/ n = m.
 Proof.
@@ -161,19 +161,19 @@ Qed.
 
 (** Dichotomy *)
 
-Notation Zle_or_lt := Z.le_gt_cases (only parsing).
+Notation Zle_or_lt := Z.le_gt_cases (compat "8.3").
 
 (** Transitivity of strict orders *)
 
-Notation Zlt_trans := Z.lt_trans (only parsing).
+Notation Zlt_trans := Z.lt_trans (compat "8.3").
 
 Lemma Zgt_trans : forall n m p:Z, n > m -> m > p -> n > p.
 Proof Zcompare_Gt_trans.
 
 (** Mixed transitivity *)
 
-Notation Zlt_le_trans := Z.lt_le_trans (only parsing).
-Notation Zle_lt_trans := Z.le_lt_trans (only parsing).
+Notation Zlt_le_trans := Z.lt_le_trans (compat "8.3").
+Notation Zle_lt_trans := Z.le_lt_trans (compat "8.3").
 
 Lemma Zle_gt_trans n m p : m <= n -> m > p -> n > p.
 Proof.
@@ -187,7 +187,7 @@ Qed.
 
 (** Transitivity of large orders *)
 
-Notation Zle_trans := Z.le_trans (only parsing).
+Notation Zle_trans := Z.le_trans (compat "8.3").
 
 Lemma Zge_trans n m p : n >= m -> m >= p -> n >= p.
 Proof.
@@ -238,8 +238,8 @@ Qed.
 
 (** Special base instances of order *)
 
-Notation Zlt_succ := Z.lt_succ_diag_r (only parsing).
-Notation Zlt_pred := Z.lt_pred_l (only parsing).
+Notation Zlt_succ := Z.lt_succ_diag_r (compat "8.3").
+Notation Zlt_pred := Z.lt_pred_l (compat "8.3").
 
 Lemma Zgt_succ n : Z.succ n > n.
 Proof.
@@ -253,8 +253,8 @@ Qed.
 
 (** Relating strict and large order using successor or predecessor *)
 
-Notation Zlt_succ_r := Z.lt_succ_r (only parsing).
-Notation Zle_succ_l := Z.le_succ_l (only parsing).
+Notation Zlt_succ_r := Z.lt_succ_r (compat "8.3").
+Notation Zle_succ_l := Z.le_succ_l (compat "8.3").
 
 Lemma Zgt_le_succ n m : m > n -> Z.succ n <= m.
 Proof.
@@ -293,10 +293,10 @@ Qed.
 
 (** Weakening order *)
 
-Notation Zle_succ := Z.le_succ_diag_r (only parsing).
-Notation Zle_pred := Z.le_pred_l (only parsing).
-Notation Zlt_lt_succ := Z.lt_lt_succ_r (only parsing).
-Notation Zle_le_succ := Z.le_le_succ_r (only parsing).
+Notation Zle_succ := Z.le_succ_diag_r (compat "8.3").
+Notation Zle_pred := Z.le_pred_l (compat "8.3").
+Notation Zlt_lt_succ := Z.lt_lt_succ_r (compat "8.3").
+Notation Zle_le_succ := Z.le_le_succ_r (compat "8.3").
 
 Lemma Zle_succ_le n m : Z.succ n <= m -> n <= m.
 Proof.
@@ -332,8 +332,8 @@ Qed.
 
 (** Special cases of ordered integers *)
 
-Notation Zlt_0_1 := Z.lt_0_1 (only parsing).
-Notation Zle_0_1 := Z.le_0_1 (only parsing).
+Notation Zlt_0_1 := Z.lt_0_1 (compat "8.3").
+Notation Zle_0_1 := Z.le_0_1 (compat "8.3").
 
 Lemma Zle_neg_pos : forall p q:positive, Zneg p <= Zpos q.
 Proof.
@@ -373,10 +373,10 @@ Qed.
 (** ** Addition *)
 (** Compatibility of addition wrt to order *)
 
-Notation Zplus_lt_le_compat := Z.add_lt_le_mono (only parsing).
-Notation Zplus_le_lt_compat := Z.add_le_lt_mono (only parsing).
-Notation Zplus_le_compat := Z.add_le_mono (only parsing).
-Notation Zplus_lt_compat := Z.add_lt_mono (only parsing).
+Notation Zplus_lt_le_compat := Z.add_lt_le_mono (compat "8.3").
+Notation Zplus_le_lt_compat := Z.add_le_lt_mono (compat "8.3").
+Notation Zplus_le_compat := Z.add_le_mono (compat "8.3").
+Notation Zplus_lt_compat := Z.add_lt_mono (compat "8.3").
 
 Lemma Zplus_gt_compat_l n m p : n > m -> p + n > p + m.
 Proof.
@@ -410,7 +410,7 @@ Qed.
 
 (** Compatibility of addition wrt to being positive *)
 
-Notation Zplus_le_0_compat := Z.add_nonneg_nonneg (only parsing).
+Notation Zplus_le_0_compat := Z.add_nonneg_nonneg (compat "8.3").
 
 (** Simplification of addition wrt to order *)
 
@@ -568,9 +568,9 @@ Qed.
 
 (** Compatibility of multiplication by a positive wrt to being positive *)
 
-Notation Zmult_le_0_compat := Z.mul_nonneg_nonneg (only parsing).
-Notation Zmult_lt_0_compat := Z.mul_pos_pos (only parsing).
-Notation Zmult_lt_O_compat := Z.mul_pos_pos (only parsing).
+Notation Zmult_le_0_compat := Z.mul_nonneg_nonneg (compat "8.3").
+Notation Zmult_lt_0_compat := Z.mul_pos_pos (compat "8.3").
+Notation Zmult_lt_O_compat := Z.mul_pos_pos (compat "8.3").
 
 Lemma Zmult_gt_0_compat n m : n > 0 -> m > 0 -> n * m > 0.
 Proof.
@@ -622,9 +622,9 @@ Qed.
 
 (** * Equivalence between inequalities *)
 
-Notation Zle_plus_swap := Z.le_add_le_sub_r (only parsing).
-Notation Zlt_plus_swap := Z.lt_add_lt_sub_r (only parsing).
-Notation Zlt_minus_simpl_swap := Z.lt_sub_pos (only parsing).
+Notation Zle_plus_swap := Z.le_add_le_sub_r (compat "8.3").
+Notation Zlt_plus_swap := Z.lt_add_lt_sub_r (compat "8.3").
+Notation Zlt_minus_simpl_swap := Z.lt_sub_pos (compat "8.3").
 
 Lemma Zeq_plus_swap n m p : n + p = m <-> n = m - p.
 Proof.
diff --git a/theories/ZArith/Zpow_def.v b/theories/ZArith/Zpow_def.v
index 6f1ebc061..4fe411584 100644
--- a/theories/ZArith/Zpow_def.v
+++ b/theories/ZArith/Zpow_def.v
@@ -14,12 +14,12 @@ Local Open Scope Z_scope.
 (** Nota : this file is mostly deprecated. The definition of [Z.pow]
     and its usual properties are now provided by module [BinInt.Z]. *)
 
-Notation Zpower_pos := Z.pow_pos (only parsing).
-Notation Zpower := Z.pow (only parsing).
-Notation Zpower_0_r := Z.pow_0_r (only parsing).
-Notation Zpower_succ_r := Z.pow_succ_r (only parsing).
-Notation Zpower_neg_r := Z.pow_neg_r (only parsing).
-Notation Zpower_Ppow := Z.pow_Zpos (only parsing).
+Notation Zpower_pos := Z.pow_pos (compat "8.3").
+Notation Zpower := Z.pow (compat "8.3").
+Notation Zpower_0_r := Z.pow_0_r (compat "8.3").
+Notation Zpower_succ_r := Z.pow_succ_r (compat "8.3").
+Notation Zpower_neg_r := Z.pow_neg_r (compat "8.3").
+Notation Zpower_Ppow := Z.pow_Zpos (compat "8.3").
 
 Lemma Zpower_theory : power_theory 1 Z.mul (@eq Z) Z.of_N Z.pow.
 Proof.
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index 27e3def4e..5d025322b 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -29,17 +29,17 @@ Proof. now apply (Z.pow_0_l (Zpos p)). Qed.
 Lemma Zpower_pos_pos x p : 0 < x -> 0 < Z.pow_pos x p.
 Proof. intros. now apply (Z.pow_pos_nonneg x (Zpos p)). Qed.
 
-Notation Zpower_1_r := Z.pow_1_r (only parsing).
-Notation Zpower_1_l := Z.pow_1_l (only parsing).
-Notation Zpower_0_l := Z.pow_0_l' (only parsing).
-Notation Zpower_0_r := Z.pow_0_r (only parsing).
-Notation Zpower_2 := Z.pow_2_r (only parsing).
-Notation Zpower_gt_0 := Z.pow_pos_nonneg (only parsing).
-Notation Zpower_ge_0 := Z.pow_nonneg (only parsing).
-Notation Zpower_Zabs := Z.abs_pow (only parsing).
-Notation Zpower_Zsucc := Z.pow_succ_r (only parsing).
-Notation Zpower_mult := Z.pow_mul_r (only parsing).
-Notation Zpower_le_monotone2 := Z.pow_le_mono_r (only parsing).
+Notation Zpower_1_r := Z.pow_1_r (compat "8.3").
+Notation Zpower_1_l := Z.pow_1_l (compat "8.3").
+Notation Zpower_0_l := Z.pow_0_l' (compat "8.3").
+Notation Zpower_0_r := Z.pow_0_r (compat "8.3").
+Notation Zpower_2 := Z.pow_2_r (compat "8.3").
+Notation Zpower_gt_0 := Z.pow_pos_nonneg (compat "8.3").
+Notation Zpower_ge_0 := Z.pow_nonneg (compat "8.3").
+Notation Zpower_Zabs := Z.abs_pow (compat "8.3").
+Notation Zpower_Zsucc := Z.pow_succ_r (compat "8.3").
+Notation Zpower_mult := Z.pow_mul_r (compat "8.3").
+Notation Zpower_le_monotone2 := Z.pow_le_mono_r (compat "8.3").
 
 Theorem Zpower_le_monotone a b c :
  0 < a -> 0 <= b <= c -> a^b <= a^c.
@@ -233,7 +233,7 @@ Qed.
 
 (** * Zsquare: a direct definition of [z^2] *)
 
-Notation Psquare := Pos.square (only parsing).
-Notation Zsquare := Z.square (only parsing).
-Notation Psquare_correct := Pos.square_spec (only parsing).
-Notation Zsquare_correct := Z.square_spec (only parsing).
+Notation Psquare := Pos.square (compat "8.3").
+Notation Zsquare := Z.square (compat "8.3").
+Notation Psquare_correct := Pos.square_spec (compat "8.3").
+Notation Zsquare_correct := Z.square_spec (compat "8.3").
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
index 9a95669f5..5b79fbce8 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -46,7 +46,7 @@ Qed.
    has been chosen to be [a], so this equation holds even for [b=0].
 *)
 
-Notation Z_quot_rem_eq := Z.quot_rem' (only parsing).
+Notation Z_quot_rem_eq := Z.quot_rem' (compat "8.3").
 
 (** Then, the inequalities constraining the remainder:
     The remainder is bounded by the divisor, in term of absolute values *)