diff options
Diffstat (limited to 'src/verilog/Value.v')
| -rw-r--r-- | src/verilog/Value.v | 4 |
1 files changed, 2 insertions, 2 deletions
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. |