diff options
Diffstat (limited to 'backend/CMparser.mly')
| -rw-r--r-- | backend/CMparser.mly | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/CMparser.mly b/backend/CMparser.mly index 1cd245ec..0b48c0f6 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -352,7 +352,7 @@ proc: fn_stackspace = $8; fn_body = $10 }) } | EXTERN STRINGLIT COLON signature - { Coq_pair($2, External({ef_id = $2; ef_sig = $4; ef_inline = false})) } + { Coq_pair($2, External(EF_external($2, $4))) } ; signature: |