diff options
Diffstat (limited to 'src/verilog/ValueInt.v')
| -rw-r--r-- | src/verilog/ValueInt.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v index 4e34c06..2220998 100644 --- a/src/verilog/ValueInt.v +++ b/src/verilog/ValueInt.v @@ -162,6 +162,7 @@ Proof. inv H. symmetry. unfold valueToPtr, ptrToValue. apply Ptrofs.of_int_to_int. trivial. Qed. -Ltac simplify_val := repeat (simplify; unfold uvalueToZ, valueToPtr, Ptrofs.of_int in *). +Ltac simplify_val := repeat (simplify; unfold uvalueToZ, valueToPtr, Ptrofs.of_int, valueToInt, intToValue, + ptrToValue in *). Ltac crush_val := simplify_val; try discriminate; try congruence; try lia; liapp; try assumption. |