From 57b71cb1bfde1832097163c7169aaf97cf8c7583 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 16:19:08 +0200
Subject: Update the extraction

---
 compiler/Extract.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'compiler/Extract.ml')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 1f9c9117..27e9a62c 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -2853,7 +2853,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 def.meta (TAssumed TResult) result_return_id ctx
+          ctx_get_variant def.meta (TAssumed TResult) result_ok_id ctx
         in
         F.pp_print_string fmt (success ^ " ())")
     | Coq ->
@@ -2884,11 +2884,11 @@ 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 def.meta (TAssumed TResult) result_return_id ctx
+          ctx_get_variant def.meta (TAssumed TResult) result_ok_id ctx
         in
         F.pp_print_string fmt (success ^ " ())")
     | HOL4 ->
-        F.pp_print_string fmt "val _ = assert_return (";
+        F.pp_print_string fmt "val _ = assert_ok (";
         F.pp_print_string fmt "“";
         let fun_name =
           ctx_get_local_function def.meta def.def_id def.loop_id ctx
-- 
cgit v1.2.3