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, 0 insertions, 2 deletions
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index c9e6d3cf3..d0075d741 100644
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -10,8 +10,6 @@
Open Local Scope nat_scope.
-Notation not_eq_sym := sym_not_eq.
-
Implicit Types m n p q : nat.
Require Import Arith_base.