aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
diff options
context:
space:
mode:
Diffstat (limited to 'powerpc')
-rw-r--r--powerpc/Asmgenproof1.v9
-rw-r--r--powerpc/SelectLongproof.v10
2 files changed, 10 insertions, 9 deletions
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index c18757b2..afbba882 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -16,6 +16,7 @@ Require Import Coqlib.
Require Import Errors.
Require Import Maps.
Require Import AST.
+Require Import Zbits.
Require Import Integers.
Require Import Floats.
Require Import Values.
@@ -80,13 +81,13 @@ Proof.
unfold Int.modu, Int.zero. decEq.
change 0 with (0 mod 65536).
change (Int.unsigned (Int.repr 65536)) with 65536.
- apply Int.eqmod_mod_eq. omega.
- unfold x, low_s. eapply Int.eqmod_trans.
- apply Int.eqmod_divides with Int.modulus.
+ apply eqmod_mod_eq. omega.
+ unfold x, low_s. eapply eqmod_trans.
+ apply eqmod_divides with Int.modulus.
unfold Int.sub. apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl.
exists 65536. compute; auto.
replace 0 with (Int.unsigned n - Int.unsigned n) by omega.
- apply Int.eqmod_sub. apply Int.eqmod_refl. apply Int.eqmod_sign_ext'.
+ apply eqmod_sub. apply eqmod_refl. apply Int.eqmod_sign_ext'.
compute; auto.
rewrite H0 in H. rewrite Int.add_zero in H.
rewrite <- H. unfold x. rewrite Int.sub_add_opp. rewrite Int.add_assoc.
diff --git a/powerpc/SelectLongproof.v b/powerpc/SelectLongproof.v
index a214d131..f16c967e 100644
--- a/powerpc/SelectLongproof.v
+++ b/powerpc/SelectLongproof.v
@@ -12,7 +12,7 @@
(** Correctness of instruction selection for 64-bit integer operations *)
-Require Import String Coqlib Maps Integers Floats Errors.
+Require Import String Coqlib Maps Zbits Integers Floats Errors.
Require Archi.
Require Import AST Values Memory Globalenvs Events.
Require Import Cminor Op CminorSel.
@@ -221,11 +221,11 @@ Proof.
change (Int64.unsigned Int64.iwordsize) with 64.
f_equal.
rewrite Int.unsigned_repr.
- apply Int.eqmod_mod_eq. omega.
- apply Int.eqmod_trans with a.
- apply Int.eqmod_divides with Int.modulus. apply Int.eqm_sym. apply Int.eqm_unsigned_repr.
+ apply eqmod_mod_eq. omega.
+ apply eqmod_trans with a.
+ apply eqmod_divides with Int.modulus. apply Int.eqm_sym. apply Int.eqm_unsigned_repr.
exists (two_p (32-6)); auto.
- apply Int.eqmod_divides with Int64.modulus. apply Int64.eqm_unsigned_repr.
+ apply eqmod_divides with Int64.modulus. apply Int64.eqm_unsigned_repr.
exists (two_p (64-6)); auto.
assert (0 <= Int.unsigned (Int.repr a) mod 64 < 64) by (apply Z_mod_lt; omega).
assert (64 < Int.max_unsigned) by (compute; auto).