diff options
Diffstat (limited to 'backend/Reloadtyping.v')
| -rw-r--r-- | backend/Reloadtyping.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v index c0051399..70d79bcb 100644 --- a/backend/Reloadtyping.v +++ b/backend/Reloadtyping.v @@ -317,6 +317,7 @@ Lemma wt_transf_code: Proof. induction c; simpl; intros. red; simpl; tauto. + rewrite transf_code_cons. apply wt_transf_instr; auto with coqlib. apply IHc. red; auto with coqlib. Qed. |