summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Extract.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index a4319482..e48e6ae6 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -2718,7 +2718,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "==";
F.pp_print_space fmt ();
let success = ctx_get_variant (TAssumed TResult) result_return_id ctx in
- F.pp_print_string fmt ("." ^ success ^ " ())")
+ F.pp_print_string fmt (success ^ " ())")
| HOL4 ->
F.pp_print_string fmt "val _ = assert_return (";
F.pp_print_string fmt "“";