diff options
Diffstat (limited to 'backend/Reloadproof.v')
| -rw-r--r-- | backend/Reloadproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index 1d49909..6402237 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -267,8 +267,8 @@ Proof. destruct s; unfold undef_getstack; unfold loc_acceptable in H; auto. apply Locmap.gso. tauto. apply Loc.diff_sym. simpl in H0; unfold t; destruct (slot_type s); tauto. - rewrite Locmap.gso. unfold undef_getstack. destruct s; auto. - apply Locmap.gso. red; congruence. + rewrite Locmap.gso. unfold undef_getstack. + destruct s; simpl in H; reflexivity || contradiction. unfold t; destruct (slot_type s); red; congruence. Qed. |