2 files changed, 11 insertions, 10 deletions
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 7f070c12..98d5bd33 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -16,7 +16,7 @@
 (* *********************************************************************)
 
 Require Import Coqlib Errors Maps.
-Require Import AST Integers Floats Values Memory Globalenvs.
+Require Import AST Zbits Integers Floats Values Memory Globalenvs.
 Require Import Op Locations Mach Conventions.
 Require Import Asm Asmgen Asmgenproof0.
 
@@ -33,16 +33,16 @@ Proof.
   predSpec Int.eq Int.eq_spec n lo.
 - auto.
 - set (m := Int.sub n lo).
-  assert (A: Int.eqmod (two_p 12) (Int.unsigned lo) (Int.unsigned n)) by (apply Int.eqmod_sign_ext'; compute; auto).
-  assert (B: Int.eqmod (two_p 12) (Int.unsigned n - Int.unsigned  lo) 0).
+  assert (A: eqmod (two_p 12) (Int.unsigned lo) (Int.unsigned n)) by (apply Int.eqmod_sign_ext'; compute; auto).
+  assert (B: eqmod (two_p 12) (Int.unsigned n - Int.unsigned  lo) 0).
   { replace 0 with (Int.unsigned n - Int.unsigned n) by omega.
-    auto using Int.eqmod_sub, Int.eqmod_refl. }
-  assert (C: Int.eqmod (two_p 12) (Int.unsigned m) 0).
-  { apply Int.eqmod_trans with (Int.unsigned n - Int.unsigned lo); auto.
-    apply Int.eqmod_divides with Int.modulus. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
+    auto using eqmod_sub, eqmod_refl. }
+  assert (C: eqmod (two_p 12) (Int.unsigned m) 0).
+  { apply eqmod_trans with (Int.unsigned n - Int.unsigned lo); auto.
+    apply eqmod_divides with Int.modulus. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
     exists (two_p (32-12)); auto. }
   assert (D: Int.modu m (Int.repr 4096) = Int.zero).
-  { apply Int.eqmod_mod_eq in C. unfold Int.modu. 
+  { apply eqmod_mod_eq in C. unfold Int.modu. 
     change (Int.unsigned (Int.repr 4096)) with (two_p 12). rewrite C. 
     reflexivity.
     apply two_p_gt_ZERO; omega. }
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index 90f077db..d12bd8af 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -20,6 +20,7 @@
 Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
+Require Import Zbits.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
@@ -372,7 +373,7 @@ Proof.
   change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl.
   apply Val.lessdef_same. f_equal. 
   transitivity (Int.repr (Z.shiftr (Int.signed i * Int.signed i0) 32)).
-  unfold Int.mulhs; f_equal. rewrite Int.Zshiftr_div_two_p by omega. reflexivity.
+  unfold Int.mulhs; f_equal. rewrite Zshiftr_div_two_p by omega. reflexivity.
   apply Int.same_bits_eq; intros n N.
   change Int.zwordsize with 32 in *.
   assert (N1: 0 <= n < 64) by omega.
@@ -400,7 +401,7 @@ Proof.
   change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl.
   apply Val.lessdef_same. f_equal. 
   transitivity (Int.repr (Z.shiftr (Int.unsigned i * Int.unsigned i0) 32)).
-  unfold Int.mulhu; f_equal. rewrite Int.Zshiftr_div_two_p by omega. reflexivity.
+  unfold Int.mulhu; f_equal. rewrite Zshiftr_div_two_p by omega. reflexivity.
   apply Int.same_bits_eq; intros n N.
   change Int.zwordsize with 32 in *.
   assert (N1: 0 <= n < 64) by omega.