diff options
Diffstat (limited to 'theories/ZArith/Zcompare.v')
| -rw-r--r-- | theories/ZArith/Zcompare.v | 26 |
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 *) |