summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-11-24 17:29:08 +0100
committerSon Ho2023-11-24 17:29:08 +0100
commit4d5d2a8628cfb002267be9a13982aa4ef24a2651 (patch)
treef96605e1ef10352b03c6e9e0eed52b66a8411607
parentfeb10e653131716698205f0b77b9623cdd1712b0 (diff)
Make a minor fix
Diffstat (limited to '')
-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 "“";