diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-01 21:09:24 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-01 21:09:24 +0100 |
| commit | 91899d674a333c429ed6cdaf6aeb24baa7cd8532 (patch) | |
| tree | 7ba6183cabe8d47668796429af36312f18663719 | |
| parent | 325b9f028f91b65e191d48dc8482da8d1ccb5d2b (diff) | |
| download | compcert-kvx-91899d674a333c429ed6cdaf6aeb24baa7cd8532.tar.gz compcert-kvx-91899d674a333c429ed6cdaf6aeb24baa7cd8532.zip | |
repr etc.
| -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. |