diff options
Diffstat (limited to 'backend/Machtyping.v')
| -rw-r--r-- | backend/Machtyping.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Machtyping.v b/backend/Machtyping.v index c2e797ae..b0673ca8 100644 --- a/backend/Machtyping.v +++ b/backend/Machtyping.v @@ -285,7 +285,7 @@ Proof. apply wt_empty_frame. econstructor; eauto. apply wt_setreg; auto. - generalize (external_call_well_typed _ _ _ _ _ _ H). + generalize (external_call_well_typed _ _ _ _ _ _ _ H). unfold proj_sig_res, Conventions.loc_result. destruct (sig_res (ef_sig ef)). destruct t0; simpl; auto. |