diff options
Diffstat (limited to 'x86/CombineOpproof.v')
| -rw-r--r-- | x86/CombineOpproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/x86/CombineOpproof.v b/x86/CombineOpproof.v index f59e582b..a7024501 100644 --- a/x86/CombineOpproof.v +++ b/x86/CombineOpproof.v @@ -125,7 +125,7 @@ Theorem combine_addr_32_sound: Proof. intros. functional inversion H; subst. (* indexed - lea *) - UseGetSound. simpl. unfold offset_addressing in H7. destruct (addressing_valid (offset_addressing_total a n)); inv H7. + UseGetSound. simpl. unfold offset_addressing in H7. destruct (addressing_valid (offset_addressing_total a n)); inv H7. eapply eval_offset_addressing_total_32; eauto. Qed. @@ -136,7 +136,7 @@ Theorem combine_addr_64_sound: Proof. intros. functional inversion H; subst. (* indexed - leal *) - UseGetSound. simpl. unfold offset_addressing in H7. destruct (addressing_valid (offset_addressing_total a n)); inv H7. + UseGetSound. simpl. unfold offset_addressing in H7. destruct (addressing_valid (offset_addressing_total a n)); inv H7. eapply eval_offset_addressing_total_64; eauto. Qed. |