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