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

4 files changed, 8 insertions, 8 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index d175c358c..648cde197 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.
diff --git a/theories/Numbers/Integer/Abstract/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v
index ce3ca21c2..4d927cb3b 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.
diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v
index 46a8a38af..ee4ea3c72 100644
--- a/theories/Numbers/Integer/Abstract/ZMulOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -173,7 +173,7 @@ Notation Zmul_neg := Zlt_mul_0 (only parsing).
 Theorem Zle_0_mul :
   forall n m : Z, 0 <= n * m -> 0 <= n /\ 0 <= m \/ n <= 0 /\ m <= 0.
 Proof.
-assert (R : forall n : Z, 0 == n <-> n == 0) by (intros; split; apply Zeq_symm).
+assert (R : forall n : Z, 0 == n <-> n == 0) by (intros; split; apply Zeq_sym).
 intros n m. repeat rewrite Zlt_eq_cases. repeat rewrite R.
 rewrite Zlt_0_mul, Zeq_mul_0.
 pose proof (Zlt_trichotomy n 0); pose proof (Zlt_trichotomy m 0). tauto.
@@ -184,7 +184,7 @@ Notation Zmul_nonneg := Zle_0_mul (only parsing).
 Theorem Zle_mul_0 :
   forall n m : Z, n * m <= 0 -> 0 <= n /\ m <= 0 \/ n <= 0 /\ 0 <= m.
 Proof.
-assert (R : forall n : Z, 0 == n <-> n == 0) by (intros; split; apply Zeq_symm).
+assert (R : forall n : Z, 0 == n <-> n == 0) by (intros; split; apply Zeq_sym).
 intros n m. repeat rewrite Zlt_eq_cases. repeat rewrite R.
 rewrite Zlt_mul_0, Zeq_mul_0.
 pose proof (Zlt_trichotomy n 0); pose proof (Zlt_trichotomy m 0). tauto.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index aa027103f..381b9baf6 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