diff options
Diffstat (limited to 'theories/ZArith/BinInt.v')
| -rw-r--r-- | theories/ZArith/BinInt.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index a5fdf855a..ad3781832 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -15,8 +15,6 @@ Require Export BinPos Pnat. Require Import BinNat Plus Mult. -Unset Boxed Definitions. - Inductive Z : Set := | Z0 : Z | Zpos : positive -> Z @@ -1002,13 +1000,13 @@ Qed. (**********************************************************************) (** * Minimum and maximum *) -Unboxed Definition Zmax (n m:Z) := +Definition Zmax (n m:Z) := match n ?= m with | Eq | Gt => n | Lt => m end. -Unboxed Definition Zmin (n m:Z) := +Definition Zmin (n m:Z) := match n ?= m with | Eq | Lt => n | Gt => m |