aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Arith
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Arith')
-rw-r--r--theories/Arith/Compare.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index d304b99bd..70bce6c53 100644
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -10,6 +10,8 @@
Local Open Scope nat_scope.
+Notation not_eq_sym := not_eq_sym (only parsing).
+
Implicit Types m n p q : nat.
Require Import Arith_base.