From a2ab81433b0da989a4c37fde92325978c858038f Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 2 Dec 2024 10:53:31 +0000 Subject: [PATCH] Fix the extracted name of some clone methods --- src/extract/ExtractBuiltin.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/extract/ExtractBuiltin.ml b/src/extract/ExtractBuiltin.ml index 85879d3f7..7572a81e6 100644 --- 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 *) @ [ mk_fun "core::clone::impls::{core::clone::Clone}::clone" - ~extract_name:(Some "core.clone.CloneBool.clone") ~can_fail:false (); + ~extract_name:(Some "core.clone.impls.CloneBool.clone") ~can_fail:false + (); ] (* Clone *) @ 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