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