From feb10e653131716698205f0b77b9623cdd1712b0 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 24 Nov 2023 17:22:33 +0100
Subject: Update some assumed type names/variants

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

(limited to 'compiler/Extract.ml')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index c8c16c08..a4319482 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -173,12 +173,7 @@ let extract_adt_g_value
          *)
         let cons =
           match variant_id with
-          | Some vid -> (
-              (* In the case of Lean, we might have to add the type name as a prefix *)
-              match (!backend, adt_id) with
-              | Lean, TAssumed _ ->
-                  ctx_get_type adt_id ctx ^ "." ^ ctx_get_variant adt_id vid ctx
-              | _ -> ctx_get_variant adt_id vid ctx)
+          | Some vid -> ctx_get_variant adt_id vid ctx
           | None -> ctx_get_struct adt_id ctx
         in
         let use_parentheses = inside && field_values <> [] in
-- 
cgit v1.2.3


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/Extract.ml')

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