aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/Zbool.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith/Zbool.v')
-rw-r--r--theories/ZArith/Zbool.v2
1 files changed, 2 insertions, 0 deletions
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. *)