diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-11 06:35:31 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-11 06:35:31 +0200 |
| commit | d336d31434602b786bcaa89c8d91d2472d9cb3f5 (patch) | |
| tree | e315eb52c474ea628b066c1108556abaad838453 /mppa_k1c/Asmblockgenproof1.v | |
| parent | d8d22519bff9414f973a1310cb32eb60e6695796 (diff) | |
| download | compcert-kvx-d336d31434602b786bcaa89c8d91d2472d9cb3f5.tar.gz compcert-kvx-d336d31434602b786bcaa89c8d91d2472d9cb3f5.zip | |
Oaddx -> P
Diffstat (limited to 'mppa_k1c/Asmblockgenproof1.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 1569aedf..86a0ff88 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1693,7 +1693,7 @@ Opaque Int.eq. 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. split; reflexivity. - (* Oshrximm *) econstructor; split. + apply exec_straight_one. simpl. eauto. |