diff options
Diffstat (limited to 'riscV')
| -rw-r--r-- | riscV/ExtValues.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v index 591507ed..0ba3b0ea 100644 --- a/riscV/ExtValues.v +++ b/riscV/ExtValues.v @@ -143,9 +143,8 @@ Qed. *) Definition bitwise_select_long b vtrue vfalse := - let b' := Int64.repr (Int64.unsigned b) in - Int64.or (Int64.and (Int64.neg b') vtrue) - (Int64.and (Int64.sub b' Int64.one) vfalse). + Int64.or (Int64.and (Int64.neg b) vtrue) + (Int64.and (Int64.sub b Int64.one) vfalse). Lemma bitwise_select_long_true : forall vtrue vfalse, @@ -166,7 +165,6 @@ Lemma bitwise_select_long_false : bitwise_select_long Int64.zero vtrue vfalse = vfalse. Proof. intros. unfold bitwise_select_long. cbn. - change (Int64.repr (Int64.unsigned Int64.zero)) with Int64.zero. rewrite Int64.neg_zero. rewrite Int64.and_commut. rewrite Int64.and_zero. |