summaryrefslogtreecommitdiff
path: root/theories/ZArith/Zbool.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith/Zbool.v')
-rw-r--r--theories/ZArith/Zbool.v4
1 files changed, 3 insertions, 1 deletions
diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v
index bb8abef4..a195b951 100644
--- a/theories/ZArith/Zbool.v
+++ b/theories/ZArith/Zbool.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Zbool.v,v 1.4.2.1 2004/07/16 19:31:21 herbelin Exp $ *)
+(* $Id: Zbool.v 6295 2004-11-12 16:40:39Z gregoire $ *)
Require Import BinInt.
Require Import Zeven.
@@ -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. *)