aboutsummaryrefslogtreecommitdiff
path: root/theories/ZArith/Zmin.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith/Zmin.v')
-rw-r--r--theories/ZArith/Zmin.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index 62a6aaf147..d7ebad1493 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