6 files changed, 14 insertions, 17 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 29e18548..0f71f2cc 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: ZBase.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+(*i $Id: ZBase.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
 
 Require Export Decidable.
 Require Export ZAxioms.
@@ -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 15beb2b9..9a17e151 100644
--- a/theories/Numbers/Integer/Abstract/ZDomain.v
+++ b/theories/Numbers/Integer/Abstract/ZDomain.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: ZDomain.v 10934 2008-05-15 21:58:20Z letouzey $ i*)
+(*i $Id: ZDomain.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
 
 Require Export NumPrelude.
 
@@ -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 e3f1d9aa..c7996ffd 100644
--- a/theories/Numbers/Integer/Abstract/ZMulOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: ZMulOrder.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+(*i $Id: ZMulOrder.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
 
 Require Export ZAddOrder.
 
@@ -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/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index cb920124..e5e950ac 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -8,7 +8,7 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: BigZ.v 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: BigZ.v 11576 2008-11-10 19:13:15Z msozeau $ i*)
 
 Require Export BigN.
 Require Import ZMulOrder.
@@ -104,8 +104,6 @@ exact sub_opp.
 exact add_opp.
 Qed.
 
-Typeclasses unfold NZadd NZmul NZsub NZeq.
-
 Add Ring BigZr : BigZring.
 
 (** Todo: tactic translating from [BigZ] to [Z] + omega *)
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 6305156b..98ad4c64 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -8,7 +8,7 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: ZMake.v 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: ZMake.v 11576 2008-11-10 19:13:15Z msozeau $ i*)
 
 Require Import ZArith.
 Require Import BigNumPrelude.
@@ -30,7 +30,6 @@ Module Make (N:NType) <: ZType.
   | Neg : N.t -> t_.
  
  Definition t := t_.
- Typeclasses unfold t.
 
  Definition zero := Pos N.zero.
  Definition one  := Pos N.one.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 8b3d815d..9427b37b 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: ZNatPairs.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+(*i $Id: ZNatPairs.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
 
 Require Import NSub. (* The most complete file for natural numbers *)
 Require Export ZMulOrder. (* The most complete file for integers *)
@@ -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