diff options
Diffstat (limited to 'kvx/SelectOpproof.v')
| -rw-r--r-- | kvx/SelectOpproof.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v index 8c834de5..7a301929 100644 --- a/kvx/SelectOpproof.v +++ b/kvx/SelectOpproof.v @@ -1199,7 +1199,6 @@ Qed. Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8). Proof. red; intros until x. unfold cast8unsigned. - rewrite Val.zero_ext_and. apply eval_andimm. compute; auto. discriminate. Qed. |