summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ExtractToFStar.ml7
1 files changed, 4 insertions, 3 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 5bf33677..0c77f48b 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -1026,7 +1026,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
let sg = def.signature in
if
sg.type_params = []
- && sg.inputs = [ unit_ty ]
+ && (sg.inputs = [ unit_ty ] || sg.inputs = [])
&& sg.outputs = [ mk_result_ty unit_ty ]
then (
(* Add a break before *)
@@ -1045,8 +1045,9 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "(";
let fun_name = ctx_get_local_function def.def_id def.back_id ctx in
F.pp_print_string fmt fun_name;
- F.pp_print_space fmt ();
- F.pp_print_string fmt "()";
+ if sg.inputs <> [] then (
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "()");
F.pp_print_space fmt ();
F.pp_print_string fmt "=";
F.pp_print_space fmt ();