diff options
Diffstat (limited to 'src/Translate.ml')
| -rw-r--r-- | src/Translate.ml | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/Translate.ml b/src/Translate.ml index 913c5cf8..3781fc33 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -371,10 +371,19 @@ let translate_module (filename : string) (dest_dir : string) let export_functions (is_rec : bool) (pure_ls : pure_fun_translation list) : unit = (* Generate the function definitions *) - let is_mut_rec = is_rec && pure_ls <> [] in let fls = List.concat (List.map (fun (fwd, back_ls) -> fwd :: back_ls) pure_ls) in + (* Check if the functions are mutually recursive - this really works + * to check if the forward and backward translations of a single + * recursive function are mutually recursive *) + let is_mut_rec = + if is_rec then + if List.length pure_ls <= 1 then + not (PureUtils.functions_not_mutually_recursive fls) + else true + else false + in List.iteri (fun i def -> let qualif = |