Merge pull request #378 from AeneasVerif/son/extract

Fix the extracted name of some clone methods
AeneasVerif · Dec 2, 2024 · 95fb853 · 95fb853
2 parents 19509e6 + a2ab814
commit 95fb853
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/src/extract/ExtractBuiltin.ml b/src/extract/ExtractBuiltin.ml
@@ -493,13 +493,16 @@ let mk_builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
   (* Clone<bool> *)
   @ [
       mk_fun "core::clone::impls::{core::clone::Clone<bool>}::clone"
-        ~extract_name:(Some "core.clone.CloneBool.clone") ~can_fail:false ();
+        ~extract_name:(Some "core.clone.impls.CloneBool.clone") ~can_fail:false
+        ();
     ]
   (* Clone<INT> *)
   @ mk_scalar_fun
       (fun ty -> "core::clone::impls::{core::clone::Clone<" ^ ty ^ ">}::clone")
       (fun ty ->
-        "core.clone.Clone" ^ StringUtils.capitalize_first_letter ty ^ ".clone")
+        "core.clone.impls.Clone"
+        ^ StringUtils.capitalize_first_letter ty
+        ^ ".clone")
       ~can_fail:false ()
   (* Lean-only definitions *)
   @ mk_lean_only