diff options
| author | Son Ho | 2022-02-09 11:43:56 +0100 |
|---|---|---|
| committer | Son Ho | 2022-02-09 11:43:56 +0100 |
| commit | 2ec238154350c6ed8b2129828292b81752d4d750 (patch) | |
| tree | 90622cbf59819d9a413c8d6917e79db9359e98aa /src/Translate.ml | |
| parent | 56b17df2da3fa60d6c20de7288cc870767576827 (diff) | |
Improve a bit the quality of the generated code by adjusting the
function suffixes depending on whether forward/backward translations
have been filtered
Diffstat (limited to '')
| -rw-r--r-- | src/Translate.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Translate.ml b/src/Translate.ml index 8084dc38..f86ef438 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -314,8 +314,8 @@ let translate_module (filename : string) (dest_dir : string) let extract_ctx = List.fold_left - (fun extract_ctx (_, def) -> - ExtractToFStar.extract_fun_def_register_names extract_ctx def) + (fun extract_ctx (keep_fwd, def) -> + ExtractToFStar.extract_fun_def_register_names extract_ctx keep_fwd def) extract_ctx trans_funs in |