2 files changed, 8 insertions, 4 deletions
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 "";