diff options
Diffstat (limited to 'src/verilog/ValueInt.v')
| -rw-r--r-- | src/verilog/ValueInt.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v index c7f69a1..4e34c06 100644 --- a/src/verilog/ValueInt.v +++ b/src/verilog/ValueInt.v @@ -161,3 +161,7 @@ Proof. unfold valueToInt. unfold intToValue in H1. auto. 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 crush_val := simplify_val; try discriminate; try congruence; try lia; liapp; try assumption. |