From 98a86e50e7dc06b77a34bf34a0476aebc07efbcd Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 12 Dec 2008 19:51:03 +0000
Subject: Uniformity with the rest of the StdLib : _symm --> _sym

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11675 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Integer/Abstract/ZDomain.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Numbers/Integer/Abstract/ZDomain.v')

diff --git a/theories/Numbers/Integer/Abstract/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v
index ce3ca21c2b..4d927cb3b6 100644
--- a/theories/Numbers/Integer/Abstract/ZDomain.v
+++ b/theories/Numbers/Integer/Abstract/ZDomain.v
@@ -49,7 +49,7 @@ assert (x == y); [rewrite Exx'; now rewrite Eyy' |
 rewrite <- H2; assert (H3 : e x y); [now apply -> eq_equiv_e | now inversion H3]]].
 Qed.
 
-Theorem neq_symm : forall n m, n # m -> m # n.
+Theorem neq_sym : forall n m, n # m -> m # n.
 Proof.
 intros n m H1 H2; symmetry in H2; false_hyp H2 H1.
 Qed.
-- 
cgit v1.2.3