From 1d8afa5949cd192620e4649ae32df49bca4da3f8 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Thu, 2 Jul 2020 21:57:03 +0100
Subject: Switch to uvalueToZ in lessdef.

---
 src/verilog/Value.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/verilog')

diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index 116986b..acabcf2 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -304,8 +304,8 @@ Inductive val_value_lessdef: val -> value -> Prop :=
     val_value_lessdef (Vint i) v'
 | val_value_lessdef_ptr:
     forall b off v',
-    off = Ptrofs.repr (valueToZ v') ->
-    (Z.modulo (valueToZ v') 4) = 0%Z ->
+    off = Ptrofs.repr (uvalueToZ v') ->
+    (Z.modulo (uvalueToZ v') 4) = 0%Z ->
     val_value_lessdef (Vptr b off) v'
 | lessdef_undef: forall v, val_value_lessdef Vundef v.
 
-- 
cgit