diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-03 22:26:06 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-03 22:26:06 +0200 |
| commit | 487fc42595bb43450f2b0b5a49b4edbc22892b9f (patch) | |
| tree | eb671c210dd1e09651003c4f0add4cca118519a2 /mppa_k1c/ExtValues.v | |
| parent | 677771949bd62f7f5bbcf99bba6b6f816f07a6c2 (diff) | |
| download | compcert-kvx-487fc42595bb43450f2b0b5a49b4edbc22892b9f.tar.gz compcert-kvx-487fc42595bb43450f2b0b5a49b4edbc22892b9f.zip | |
rm old select/selectl/selectf/selectfs
Diffstat (limited to 'mppa_k1c/ExtValues.v')
| -rw-r--r-- | mppa_k1c/ExtValues.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v index 155afa83..8e6aa028 100644 --- a/mppa_k1c/ExtValues.v +++ b/mppa_k1c/ExtValues.v @@ -287,10 +287,10 @@ Proof. intros. apply Int.eqm_samerepr. unfold Int.eqm. - unfold Int.eqmod. + unfold Zbits.eqmod. pose proof (Int64.eqm_unsigned_repr x) as H64. unfold Int64.eqm in H64. - unfold Int64.eqmod in H64. + unfold Zbits.eqmod in H64. destruct H64 as [k64 H64]. change Int64.modulus with 18446744073709551616 in *. change Int.modulus with 4294967296. @@ -367,7 +367,7 @@ Proof. apply Int.eqm_samerepr. unfold Int.eqm. change (Int64.unsigned (Int64.repr (-2147483648))) with 18446744071562067968. - unfold Int.eqmod. + unfold Zbits.eqmod. change Int.modulus with 4294967296. exists (-4294967296). compute. |