5 files changed, 8 insertions, 3 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 10e7def9e..16e2ff325 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -17,6 +17,8 @@ Require Export Pnat.
 Require Import BinNat.
 Require Import Plus.
 Require Import Mult.
+
+Unset Boxed Definitions.
 (**********************************************************************)
 (** Binary integer numbers *)
 
@@ -1035,4 +1037,4 @@ Definition Zabs_N (z:Z) :=
 Definition Z_of_N (x:N) := match x with
                            | N0 => Z0
                            | Npos p => Zpos p
-                           end.
-\ No newline at end of file
+                           end.
diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v
index bc92eca14..d49bbfc68 100644
--- a/theories/ZArith/Zbool.v
+++ b/theories/ZArith/Zbool.v
@@ -15,6 +15,8 @@ Require Import Zcompare.
 Require Import ZArith_dec.
 Require Import Sumbool.
 
+Unset Boxed Definitions.
+
 (** The decidability of equality and order relations over
     type [Z] give some boolean functions with the adequate specification. *)
 
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index c4dca7121..025e03d4a 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -36,7 +36,7 @@ Open Local Scope Z_scope.
   
 *)
 
-Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) {struct a} : 
+Unboxed Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) {struct a} : 
  Z * Z :=
   match a with
   | xH => if Zge_bool b 2 then (0, 1) else (1, 0)
diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v
index 25b05cdc7..c45355133 100644
--- a/theories/ZArith/Zlogarithm.v
+++ b/theories/ZArith/Zlogarithm.v
@@ -36,6 +36,7 @@ Fixpoint log_inf (p:positive) : Z :=
   | xO q => Zsucc (log_inf q)	(* 2n *)
   | xI q => Zsucc (log_inf q)	(* 2n+1 *)
   end.
+
 Fixpoint log_sup (p:positive) : Z :=
   match p with
   | xH => 0	(* 1 *)
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index 62a6aaf14..d7ebad149 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -19,7 +19,7 @@ Open Local Scope Z_scope.
 (**********************************************************************)
 (** Minimum on binary integer numbers *)
 
-Definition Zmin (n m:Z) :=
+Unboxed Definition Zmin (n m:Z) :=
   match n ?= m return Z with
   | Eq => n
   | Lt => n