diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Translate.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/Translate.ml b/src/Translate.ml index 9b748461..7e4e6178 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -657,9 +657,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) (* Extract the opaque functions, if needed *) let opaque_funs_module = if has_opaque_funs then ( - let opaque_filename = - extract_filebasename ^ ".Opaque" ^ types_filename_ext - in + let opaque_filename = extract_filebasename ^ ".Opaque.fsti" in let opaque_module = module_name ^ ".Opaque" in let opaque_config = { @@ -667,6 +665,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) extract_fun_decls = true; extract_transparent = false; extract_opaque = true; + interface = true; } in extract_file opaque_config gen_ctx opaque_filename m.M.name |