diff options
Diffstat (limited to 'cfrontend/Cminorgenproof.v')
| -rw-r--r-- | cfrontend/Cminorgenproof.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index bc1c92ca..ed45ac23 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -875,7 +875,6 @@ Proof. intros. apply Mem.perm_implies with Freeable; auto with mem. eapply Mem.perm_alloc_2; eauto. instantiate (1 := f1). red; intros. eelim Mem.fresh_block_alloc; eauto. eapply Mem.valid_block_inject_2; eauto. - intros. apply PTree.gempty. eapply match_callstack_alloc_right; eauto. intros. destruct (In_dec peq id (map fst vars)). apply cenv_remove_gss; auto. |