From e6e749d47f05a6d48625c305b6af132440382efb Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 16 Sep 2023 21:54:48 +0200
Subject: Fix more issues

---
 compiler/Extract.ml     | 13 ++++++-------
 compiler/ExtractBase.ml |  2 +-
 2 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 60455cd9..ecfb47c7 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -732,21 +732,20 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
   in
 
   let trait_decl_name (trait_decl : trait_decl) : string =
-    type_name_to_snake_case trait_decl.name
+    type_name trait_decl.name
   in
 
   let trait_impl_name (trait_decl : trait_decl) (trait_impl : trait_impl) :
       string =
     (* TODO: provisional: we concatenate the trait impl name (which is its type)
        with the trait decl name *)
-    let inst_keyword =
+    let trait_decl =
+      let name = trait_decl.name in
       match !backend with
-      | HOL4 | FStar | Coq -> "_instance"
-      | Lean -> "Instance"
+      | FStar | Coq | HOL4 -> type_name_to_snake_case name ^ "_instance"
+      | Lean -> String.concat "" (get_type_name name) ^ "Instance"
     in
-    flatten_name
-      (get_type_name trait_impl.name
-      @ [ trait_decl_name trait_decl ^ inst_keyword ])
+    flatten_name (get_type_name trait_impl.name @ [ trait_decl ])
   in
 
   let trait_parent_clause_name (trait_decl : trait_decl) (clause : trait_clause)
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 1996d38f..28928325 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1339,7 +1339,7 @@ let ctx_add_trait_method (d : trait_decl) (item_name : string) (f : fun_decl)
   (* Add a prefix if necessary *)
   let name =
     if !Config.record_fields_short_names then name
-    else ctx.fmt.trait_decl_name d ^ name
+    else ctx.fmt.trait_decl_name d ^ "_" ^ name
   in
   let is_opaque = false in
   ctx_add is_opaque (TraitMethodId (d.def_id, item_name, f.back_id)) name ctx
-- 
cgit v1.2.3