4 files changed, 13 insertions, 13 deletions
diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v
index f58b87d8..91ae5b70 100644
--- a/theories/Numbers/Natural/Abstract/NAdd.v
+++ b/theories/Numbers/Natural/Abstract/NAdd.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: NAdd.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+(*i $Id: NAdd.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
 
 Require Export NBase.
 
@@ -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 3e4032b5..85e2c2ab 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: NBase.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+(*i $Id: NBase.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
 
 Require Export Decidable.
 Require Export NAxioms.
@@ -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 e15e4672..0a8f5f1e 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: NDefOps.v 11039 2008-06-02 23:26:13Z letouzey $ i*)
+(*i $Id: NDefOps.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
 
 Require Import Bool. (* To get the orb and negb function *)
 Require Export NStrongRec.
@@ -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 031dbdea..c6a6da48 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: NStrongRec.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+(*i $Id: NStrongRec.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
 
 (** This file defined the strong (course-of-value, well-founded) recursion
 and proves its properties *)
@@ -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.