diff options
Diffstat (limited to 'arm/Op.v')
-rw-r--r-- | arm/Op.v | 3 |
1 files changed, 1 insertions, 2 deletions
@@ -572,8 +572,7 @@ Proof. destruct v; destruct chunk; exact I. intros until v. unfold Mem.loadv. destruct addr; intros; try discriminate. - generalize (Mem.load_inv _ _ _ _ _ H0). - intros [X Y]. subst v. apply H. + eapply Mem.load_type; eauto. Qed. End SOUNDNESS. |