From 4d5d2a8628cfb002267be9a13982aa4ef24a2651 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 24 Nov 2023 17:29:08 +0100 Subject: Make a minor fix --- compiler/Extract.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'compiler') 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 "“"; -- cgit v1.2.3