diff options
Diffstat (limited to 'backend/Linearizetyping.v')
| -rw-r--r-- | backend/Linearizetyping.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Linearizetyping.v b/backend/Linearizetyping.v index 7393535d..b4e25de7 100644 --- a/backend/Linearizetyping.v +++ b/backend/Linearizetyping.v @@ -71,9 +71,9 @@ Lemma wt_linearize_body: forall enum, wt_code f.(LTL.fn_sig) (linearize_body f enum). Proof. - induction enum; simpl. + unfold linearize_body; induction enum; rewrite list_fold_right_eq. red; simpl; intros; contradiction. - caseEq ((LTL.fn_code f)!a); intros. + unfold linearize_node. caseEq ((LTL.fn_code f)!a); intros. apply wt_add_instr. constructor. apply wt_linearize_instr; eauto with coqlib. auto. Qed. |