From da1f4c0824fc816fa0de124e0fc9a42a9112c1f1 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 11 Jan 2026 11:44:42 +0000 Subject: [PATCH 1/2] Update following changes in Charon-ML --- lib/AstOfLlbc.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index 8c392013..3709bd6b 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -1227,7 +1227,9 @@ let rec mk_clause_binders_and_args env ?depth ?clause_ref (trait_clauses : C.tra the trait, we must substitute them with the given generics. We should in principle substitute everything but we currently don't. This will likely be a source of bugs. *) - let subst = Charon.Substitute.make_subst_from_generics trait_decl.generics trait_generics in + let subst = + Charon.Substitute.make_subst_from_generics trait_decl.generics trait_generics Self + in let substitute_visitor = Charon.Substitute.st_substitute_visitor in let name = string_of_name env trait_decl.item_meta.name in @@ -1615,7 +1617,7 @@ let rec expression_of_fn_ptr env depth (fn_ptr : C.fn_ptr) = trait_impl.methods @ build_trait_ref_mapping (" " ^ depth) (let subst = - Charon.Substitute.make_subst_from_generics trait_impl.generics _generics + Charon.Substitute.make_subst_from_generics trait_impl.generics _generics Self in (*_generics.trait_refs*) List.map From f565a1cac7ddbb00975fc7ee4d8497bea843405f Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 11 Jan 2026 11:44:49 +0000 Subject: [PATCH 2/2] Update the Charon pin --- flake.lock | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/flake.lock b/flake.lock index 23f4b90e..27e6115a 100644 --- a/flake.lock +++ b/flake.lock @@ -26,11 +26,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1767093296, - "narHash": "sha256-xVO/cOWzKJFcht6tkqXA9aErR02Xdj4XxKDgt5Gn54Q=", + "lastModified": 1768082582, + "narHash": "sha256-9H8ggZm5I+A4anR8jQiomkDWCo3WTqIex6ylKNhyvnw=", "owner": "aeneasverif", "repo": "charon", - "rev": "e587fcdad522736b216c23563cb6a7715450844d", + "rev": "6c6b93beebaf143d9a6d3ffd0f7fc0ffbf57efe4", "type": "github" }, "original": {