diff options
Diffstat (limited to 'kvx/Asmblockgenproof1.v')
-rw-r--r-- | kvx/Asmblockgenproof1.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kvx/Asmblockgenproof1.v b/kvx/Asmblockgenproof1.v index 259c4f9c..a18afec8 100644 --- a/kvx/Asmblockgenproof1.v +++ b/kvx/Asmblockgenproof1.v @@ -1521,14 +1521,14 @@ Opaque Int.eq. repeat split; intros; simpl; Simpl. assert (A: Int.ltu (Int.repr 24) Int.iwordsize = true) by auto. destruct (rs x0); auto; simpl. rewrite A; simpl. Simpl. unfold Val.shr. rewrite A. - apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. + apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. compute; intuition congruence. - (* Ocast16signed *) econstructor; split. eapply exec_straight_two. simpl;eauto. simpl;eauto. repeat split; intros; Simpl. assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto. destruct (rs x0); auto; simpl. rewrite A; simpl. Simpl. unfold Val.shr. rewrite A. - apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. + apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. compute; intuition congruence. - (* Oshrximm *) econstructor; split. + apply exec_straight_one. simpl. eauto. |