diff options
Diffstat (limited to 'cfrontend/Csharpminor.v')
| -rw-r--r-- | cfrontend/Csharpminor.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index 2fddc6c2..4c61918d 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.v @@ -516,7 +516,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (State f f.(fn_body) k e m2) | step_external_function: forall ef vargs k m t vres m', - external_call ef vargs m t vres m' -> + external_call ef (Genv.find_symbol ge) vargs m t vres m' -> step (Callstate (External ef) vargs k m) t (Returnstate vres k m') |