diff options
Diffstat (limited to 'backend/Linearizeproof.v')
| -rw-r--r-- | backend/Linearizeproof.v | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index 8378332..b385429 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -604,22 +604,6 @@ Proof. destruct (Genv.find_symbol ge i); try discriminate. eapply Genv.find_funct_ptr_prop; eauto. - (* Lalloc *) - destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. - simpl in EQ. subst c. - assert (REACH': (reachable f)!!pc' = true). - eapply reachable_successors; eauto. - unfold successors; rewrite H; auto with coqlib. - exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT']. - econstructor; split. - eapply plus_left'. - eapply exec_Lalloc; eauto. - eapply add_branch_correct; eauto. - eapply is_tail_add_branch. eapply is_tail_cons_left. - eapply is_tail_find_label. eauto. - traceEq. - econstructor; eauto. - (* Lcond true *) destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. simpl in EQ. subst c. |