diff --git a/charon-pin b/charon-pin
index 974d946d5..fe78caa2b 100644
--- a/charon-pin
+++ b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-1ec8d4bb0116abf4486bac234ac01acf84e2a83a
+09043b10a0de68a87e55f8789cb98e1f16fe5b11
diff --git a/flake.lock b/flake.lock
index ed9708732..1e139af1a 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1778681500,
-        "narHash": "sha256-AQYuEdqZFzVEfOsOC4cOasLHPtPk9J9RY3cnS8we4Wg=",
+        "lastModified": 1779805263,
+        "narHash": "sha256-bq9Noz1r4AzKi1BMbkS4xzJA+yyRr+HNm57qPdyeQ+Q=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "1ec8d4bb0116abf4486bac234ac01acf84e2a83a",
+        "rev": "09043b10a0de68a87e55f8789cb98e1f16fe5b11",
         "type": "github"
       },
       "original": {
diff --git a/tests/lean/MultiTarget.lean b/tests/lean/MultiTarget.lean
index 53e5433f4..c3624ab5e 100644
--- a/tests/lean/MultiTarget.lean
+++ b/tests/lean/MultiTarget.lean
@@ -35,7 +35,7 @@ def x86.Sse2.Insts.Multi_targetSimdTraitU128.add
   (a : Std.U128) (b : Std.U128) : Result Std.U128 := do
   ok (core.num.U128.wrapping_add a b)
 
-/-- Trait implementation: [multi_target::x86::{multi_target::SimdTrait<u128> for multi_target::x86::Sse2}::x86_64-apple-darwin]
+/-- Trait implementation: [multi_target::x86::{multi_target::SimdTrait<u128> for multi_target::x86::Sse2}]
     Source: 'tests/src/multi-target.rs', lines 16:4-22:5 -/
 @[reducible]
 def x86.Sse2.Insts.Multi_targetSimdTraitU128 : SimdTrait x86.Sse2 Std.U128 := {
@@ -55,7 +55,7 @@ def arm.Neon.Insts.Multi_targetSimdTraitU128.add
   (a : Std.U128) (b : Std.U128) : Result Std.U128 := do
   ok (core.num.U128.wrapping_add a b)
 
-/-- Trait implementation: [multi_target::arm::{multi_target::SimdTrait<u128> for multi_target::arm::Neon}::aarch64-apple-darwin]
+/-- Trait implementation: [multi_target::arm::{multi_target::SimdTrait<u128> for multi_target::arm::Neon}]
     Source: 'tests/src/multi-target.rs', lines 31:4-37:5 -/
 @[reducible]
 def arm.Neon.Insts.Multi_targetSimdTraitU128 : SimdTrait arm.Neon Std.U128 := {