diff options
Diffstat (limited to 'theories/Arith/Compare_dec.v')
| -rw-r--r-- | theories/Arith/Compare_dec.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 1e3237d10..b7235b669 100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -133,11 +133,11 @@ Qed. See now [Nat.compare] and its properties. In scope [nat_scope], the notation for [Nat.compare] is "?=" *) -Notation nat_compare := Nat.compare (compat "8.4"). +Notation nat_compare := Nat.compare (compat "8.6"). -Notation nat_compare_spec := Nat.compare_spec (compat "8.4"). -Notation nat_compare_eq_iff := Nat.compare_eq_iff (compat "8.4"). -Notation nat_compare_S := Nat.compare_succ (compat "8.4"). +Notation nat_compare_spec := Nat.compare_spec (compat "8.6"). +Notation nat_compare_eq_iff := Nat.compare_eq_iff (compat "8.6"). +Notation nat_compare_S := Nat.compare_succ (only parsing). Lemma nat_compare_lt n m : n<m <-> (n ?= m) = Lt. Proof. @@ -198,9 +198,9 @@ Qed. See now [Nat.leb] and its properties. In scope [nat_scope], the notation for [Nat.leb] is "<=?" *) -Notation leb := Nat.leb (compat "8.4"). +Notation leb := Nat.leb (only parsing). -Notation leb_iff := Nat.leb_le (compat "8.4"). +Notation leb_iff := Nat.leb_le (only parsing). Lemma leb_iff_conv m n : (n <=? m) = false <-> m < n. Proof. |