aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ZUtil
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/ZUtil')
-rw-r--r--src/Util/ZUtil/Definitions.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v
index 2c87a9497..67ccbc772 100644
--- a/src/Util/ZUtil/Definitions.v
+++ b/src/Util/ZUtil/Definitions.v
@@ -17,7 +17,7 @@ Module Z.
Definition cc_m s x := if dec (2 ^ (Z.log2 s) = s) then x >> (Z.log2 s - 1) else x / (s / 2).
(* least significant bit *)
- Definition cc_l x := Z.land x (Z.ones 1).
+ Definition cc_l x := x mod 2.
(* two-register right shift *)
Definition rshi s hi lo n :=