diff options
Diffstat (limited to 'compiler/Extract.ml')
| -rw-r--r-- | compiler/Extract.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 3429cd11..46cf8c4a 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -1332,7 +1332,9 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter) in let fwd_back_comment = match def.back_id with - | None -> [ "forward function" ] + | None -> + if !Config.return_back_funs then [ "function definition" ] + else [ "forward function" ] | Some id -> (* Check if there is only one backward function, and no forward function *) if (not keep_fwd) && num_backs = 1 then |