diff options
Diffstat (limited to 'riscV/SelectOpproof.v')
| -rw-r--r-- | riscV/SelectOpproof.v | 5 |
1 files changed, 3 insertions, 2 deletions
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. |