aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/Znumtheory.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith/Znumtheory.v')
-rw-r--r--theories/ZArith/Znumtheory.v62
1 files changed, 31 insertions, 31 deletions
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.