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/NatPairs/ZNatPairs.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories/Numbers/Integer/NatPairs')

diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index aa027103fb..381b9baf61 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -110,7 +110,7 @@ Proof.
 unfold reflexive, Zeq. reflexivity.
 Qed.
 
-Theorem ZE_symm : symmetric Z Zeq.
+Theorem ZE_sym : symmetric Z Zeq.
 Proof.
 unfold symmetric, Zeq; now symmetry.
 Qed.
@@ -127,7 +127,7 @@ Qed.
 
 Theorem NZeq_equiv : equiv Z Zeq.
 Proof.
-unfold equiv; repeat split; [apply ZE_refl | apply ZE_trans | apply ZE_symm].
+unfold equiv; repeat split; [apply ZE_refl | apply ZE_trans | apply ZE_sym].
 Qed.
 
 Add Relation Z Zeq
-- 
cgit v1.2.3