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

11 files changed, 21 insertions, 21 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
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 0b917e998..985466979 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -15,7 +15,7 @@ Require Import NZAxioms.
 Module NZBasePropFunct (Import NZAxiomsMod : NZAxiomsSig).
 Open Local Scope NatIntScope.
 
-Theorem NZneq_symm : forall n m : NZ, n ~= m -> m ~= n.
+Theorem NZneq_sym : forall n m : NZ, n ~= m -> m ~= n.
 Proof.
 intros n m H1 H2; symmetry in H2; false_hyp H2 H1.
 Qed.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index d8eaeb99c..8747a4c44 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -118,7 +118,7 @@ Qed.
 
 Theorem NZneq_succ_diag_r : forall n : NZ, n ~= S n.
 Proof.
-intro n; apply NZneq_symm; apply NZneq_succ_diag_l.
+intro n; apply NZneq_sym; apply NZneq_succ_diag_l.
 Qed.
 
 Theorem NZnlt_succ_diag_l : forall n : NZ, ~ S n < n.
diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v
index 37244159f..58dddfcf9 100644
--- a/theories/Numbers/Natural/Abstract/NAdd.v
+++ b/theories/Numbers/Natural/Abstract/NAdd.v
@@ -103,7 +103,7 @@ Qed.
 Theorem succ_add_discr : forall n m : N, m ~= S (n + m).
 Proof.
 intro n; induct m.
-apply neq_symm. apply neq_succ_0.
+apply neq_sym. apply neq_succ_0.
 intros m IH H. apply succ_inj in H. rewrite add_succ_r in H.
 unfold not in IH; now apply IH.
 Qed.
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 0d7bc63eb..deee349ca 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -48,14 +48,14 @@ Proof pred_0.
 Theorem Neq_refl : forall n : N, n == n.
 Proof (proj1 NZeq_equiv).
 
-Theorem Neq_symm : forall n m : N, n == m -> m == n.
+Theorem Neq_sym : forall n m : N, n == m -> m == n.
 Proof (proj2 (proj2 NZeq_equiv)).
 
 Theorem Neq_trans : forall n m p : N, n == m -> m == p -> n == p.
 Proof (proj1 (proj2 NZeq_equiv)).
 
-Theorem neq_symm : forall n m : N, n ~= m -> m ~= n.
-Proof NZneq_symm.
+Theorem neq_sym : forall n m : N, n ~= m -> m ~= n.
+Proof NZneq_sym.
 
 Theorem succ_inj : forall n1 n2 : N, S n1 == S n2 -> n1 == n2.
 Proof NZsucc_inj.
@@ -111,7 +111,7 @@ Qed.
 
 Theorem neq_0_succ : forall n : N, 0 ~= S n.
 Proof.
-intro n; apply neq_symm; apply neq_succ_0.
+intro n; apply neq_sym; apply neq_succ_0.
 Qed.
 
 (* Next, we show that all numbers are nonnegative and recover regular induction
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index 57d33e7b6..e18e3b67f 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -243,7 +243,7 @@ Definition E2 := prod_rel Neq Neq.
 
 Add Relation (prod N N) E2
 reflexivity proved by (prod_rel_refl N N Neq Neq E_equiv E_equiv)
-symmetry proved by (prod_rel_symm N N Neq Neq E_equiv E_equiv)
+symmetry proved by (prod_rel_sym N N Neq Neq E_equiv E_equiv)
 transitivity proved by (prod_rel_trans N N Neq Neq E_equiv E_equiv)
 as E2_rel.
 
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index 5303bf8e5..a9eec350f 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -81,9 +81,9 @@ Proof.
 intros n1 n2 H. unfold g. now apply strong_rec_wd.
 Qed.
 
-Theorem NtoA_eq_symm : symmetric (N -> A) (fun_eq Neq Aeq).
+Theorem NtoA_eq_sym : symmetric (N -> A) (fun_eq Neq Aeq).
 Proof.
-apply fun_eq_symm.
+apply fun_eq_sym.
 exact (proj2 (proj2 NZeq_equiv)).
 exact (proj2 (proj2 Aeq_equiv)).
 Qed.
@@ -97,7 +97,7 @@ exact (proj1 (proj2 Aeq_equiv)).
 Qed.
 
 Add Relation (N -> A) (fun_eq Neq Aeq)
- symmetry proved by NtoA_eq_symm
+ symmetry proved by NtoA_eq_sym
  transitivity proved by NtoA_eq_trans
 as NtoA_eq_rel.
 
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index 904145d50..14ea812f3 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -212,7 +212,7 @@ unfold reflexive, prod_rel.
 destruct x; split; [apply (proj1 EA_equiv) | apply (proj1 EB_equiv)]; simpl.
 Qed.
 
-Lemma prod_rel_symm : symmetric (A * B) prod_rel.
+Lemma prod_rel_sym : symmetric (A * B) prod_rel.
 Proof.
 unfold symmetric, prod_rel.
 destruct x; destruct y;
@@ -229,7 +229,7 @@ Qed.
 
 Theorem prod_rel_equiv : equiv (A * B) prod_rel.
 Proof.
-unfold equiv; split; [exact prod_rel_refl | split; [exact prod_rel_trans | exact prod_rel_symm]].
+unfold equiv; split; [exact prod_rel_refl | split; [exact prod_rel_trans | exact prod_rel_sym]].
 Qed.
 
 End RelationOnProduct.