4 files changed, 6 insertions, 1 deletions
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 947dc818e1..bb2c01437d 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -102,6 +102,8 @@ 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 cbf6f701f2..5376027ddb 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -30,6 +30,7 @@ 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/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 485480fa04..1e0b45cd2c 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -76,6 +76,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 0baba94c6d..c360f53dc8 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -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 "";