aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/BinInt.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith/BinInt.v')
-rw-r--r--theories/ZArith/BinInt.v4
1 files changed, 3 insertions, 1 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.