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/ZBase.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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

diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index d175c358cd..648cde1978 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -36,14 +36,14 @@ Proof NZpred_succ.
 Theorem Zeq_refl : forall n : Z, n == n.
 Proof (proj1 NZeq_equiv).
 
-Theorem Zeq_symm : forall n m : Z, n == m -> m == n.
+Theorem Zeq_sym : forall n m : Z, n == m -> m == n.
 Proof (proj2 (proj2 NZeq_equiv)).
 
 Theorem Zeq_trans : forall n m p : Z, n == m -> m == p -> n == p.
 Proof (proj1 (proj2 NZeq_equiv)).
 
-Theorem Zneq_symm : forall n m : Z, n ~= m -> m ~= n.
-Proof NZneq_symm.
+Theorem Zneq_sym : forall n m : Z, n ~= m -> m ~= n.
+Proof NZneq_sym.
 
 Theorem Zsucc_inj : forall n1 n2 : Z, S n1 == S n2 -> n1 == n2.
 Proof NZsucc_inj.
-- 
cgit v1.2.3