diff options
Diffstat (limited to 'mppa_k1c/Asmblockgenproof1.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 00df01e3..9c836037 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1535,7 +1535,6 @@ Opaque Int.eq. + apply exec_straight_one. simpl. eauto. + repeat split. * rewrite Pregmap.gss. - subst v. destruct (rs x0); simpl; trivial. unfold Val.maketotal. destruct (Int.ltu _ _); simpl; trivial. @@ -1546,7 +1545,6 @@ Opaque Int.eq. + apply exec_straight_one. simpl. eauto. + repeat split. * rewrite Pregmap.gss. - subst v. destruct (rs x0); simpl; trivial. unfold Val.maketotal. destruct (Int.ltu _ _); simpl; trivial. |