diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ExtractToFStar.ml | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index d1e1176c..0781a811 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -310,7 +310,11 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) if tys = [] then F.pp_print_string fmt "unit" else ( F.pp_print_string fmt "("; - Collections.List.iter_link (F.pp_print_space fmt) + Collections.List.iter_link + (fun () -> + F.pp_print_space fmt (); + F.pp_print_string fmt "&"; + F.pp_print_space fmt ()) (extract_ty ctx fmt true) tys; F.pp_print_string fmt ")") | AdtId _ | Assumed _ -> @@ -956,6 +960,11 @@ let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter) ctx) ctx def.inputs_lvs in + (* Print the return type *) + F.pp_print_space fmt (); + F.pp_print_string fmt ":"; + F.pp_print_space fmt (); + extract_ty ctx fmt false (Collections.List.to_cons_nil def.signature.outputs); (* Print the "=" *) F.pp_print_space fmt (); F.pp_print_string fmt "="; |