4 files changed, 15 insertions, 12 deletions
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index 826ffa2c..15aed7ab 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: NOrder.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+(*i $Id: NOrder.v 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 Require Export NMul.
 
@@ -309,13 +309,12 @@ Proof NZgt_wf.
 
 Theorem lt_wf_0 : well_founded lt.
 Proof.
-assert (H : relations_eq lt (fun n m : N => 0 <= n /\ n < m)).
+setoid_replace lt with (fun n m : N => 0 <= n /\ n < m) 
+  using relation (@relations_eq N N).
+apply lt_wf.
 intros x y; split.
 intro H; split; [apply le_0_l | assumption]. now intros [_ H].
-rewrite H; apply lt_wf.
-(* does not work:
-setoid_replace lt with (fun n m : N => 0 <= n /\ n < m) using relation relations_eq.*)
-Qed.
+Defined.
 
 (* Theorems that are true for natural numbers but not for integers *)
 
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 0574c09f..41c255b1 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: BigN.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+(*i $Id: BigN.v 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 (** * Natural numbers in base 2^31 *)
 
@@ -47,6 +47,8 @@ Infix "?=" := BigN.compare : bigN_scope.
 Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope.
 Infix "<" := BigN.lt : bigN_scope.
 Infix "<=" := BigN.le : bigN_scope.
+Notation "x > y" := (BigN.lt y x)(only parsing) : bigN_scope.
+Notation "x >= y" := (BigN.le y x)(only parsing) : bigN_scope.
 Notation "[ i ]" := (BigN.to_Z i) : bigN_scope.
 
 Open Scope bigN_scope.
@@ -62,7 +64,7 @@ Qed.
 
 (** [BigN] is a semi-ring *)
 
-Lemma BigNring : 
+Lemma BigNring :
  semi_ring_theory BigN.zero BigN.one BigN.add BigN.mul BigN.eq.
 Proof.
 constructor.
@@ -76,6 +78,8 @@ exact mul_assoc.
 exact mul_add_distr_r.
 Qed.
 
+Typeclasses unfold NZadd NZsub NZmul.
+
 Add Ring BigNr : BigNring.
 
 (** Todo: tactic translating from [BigN] to [Z] + omega *)
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index bd0fb5b1..4d6b45c5 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -8,7 +8,7 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-(*i $Id: NMake_gen.ml 11136 2008-06-18 10:41:34Z herbelin $ i*)
+(*i $Id: NMake_gen.ml 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 (*S NMake_gen.ml : this file generates NMake.v *)
 
@@ -139,7 +139,7 @@ let _ =
   pr "";
   pr " Definition %s := %s_." t t;
   pr "";
-
+  pr " Typeclasses unfold %s." t;
   pr " Definition w_0 := w0_op.(znz_0).";
   pr "";
 
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index fe068437..84836268 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: NSigNAxioms.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+(*i $Id: NSigNAxioms.v 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 Require Import ZArith.
 Require Import Nnat.
@@ -223,7 +223,7 @@ Qed.
 Add Morphism N.compare with signature N.eq ==> N.eq ==> (@eq comparison) as compare_wd.
 Proof. 
 intros x x' Hx y y' Hy.
-rewrite 2 spec_compare_alt; rewrite Hx, Hy; intuition.
+rewrite 2 spec_compare_alt. unfold N.eq in *. rewrite Hx, Hy; intuition.
 Qed.
 
 Add Morphism N.lt with signature N.eq ==> N.eq ==> iff as NZlt_wd.