aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Arith/EqNat.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Arith/EqNat.v')
-rw-r--r--theories/Arith/EqNat.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 722615428..a4f2d30bd 100644
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -69,10 +69,10 @@ Defined.
We reuse the one already defined in module [Nat].
In scope [nat_scope], the notation "=?" can be used. *)
-Notation beq_nat := Nat.eqb (compat "8.4").
+Notation beq_nat := Nat.eqb (only parsing).
-Notation beq_nat_true_iff := Nat.eqb_eq (compat "8.4").
-Notation beq_nat_false_iff := Nat.eqb_neq (compat "8.4").
+Notation beq_nat_true_iff := Nat.eqb_eq (only parsing).
+Notation beq_nat_false_iff := Nat.eqb_neq (only parsing).
Lemma beq_nat_refl n : true = (n =? n).
Proof.