diff options
Diffstat (limited to 'cfrontend/Cshmgen.v')
| -rw-r--r-- | cfrontend/Cshmgen.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index cc81d0f..56bef55 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -620,8 +620,8 @@ Definition transl_fundef (f: Csyntax.fundef) : res fundef := match f with | Csyntax.Internal g => do tg <- transl_function g; OK(AST.Internal tg) - | Csyntax.External id args res => - OK(AST.External (external_function id args res)) + | Csyntax.External ef args res => + OK(AST.External ef) end. (** ** Translation of programs *) |