diff --git a/flake.lock b/flake.lock
index 76230189..e4f533f8 100644
--- a/flake.lock
+++ b/flake.lock
@@ -26,11 +26,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1763567718,
-        "narHash": "sha256-95sNs1hcFy77Cwllj5KjtghVjaqdKw7dfr2gtyLHTcA=",
+        "lastModified": 1764078511,
+        "narHash": "sha256-ZI/5ynYf/2zKNQaRJbKwyePpBcraqv1flbgRgcYfvDc=",
         "owner": "AeneasVerif",
         "repo": "charon",
-        "rev": "69f63d6094105bf7f354c82696e5ac9424440e8a",
+        "rev": "637a6bc8a4c2a79875af5aa4e413c7ef3aa7f391",
         "type": "github"
       },
       "original": {
@@ -680,17 +680,17 @@
         ]
       },
       "locked": {
-        "lastModified": 1762569282,
-        "narHash": "sha256-vINZAJpXQTZd5cfh06Rcw7hesH7sGSvi+Tn+HUieJn8=",
+        "lastModified": 1763952169,
+        "narHash": "sha256-+PeDBD8P+NKauH+w7eO/QWCIp8Cx4mCfWnh9sJmy9CM=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "a35a6144b976f70827c2fe2f5c89d16d8f9179d8",
+        "rev": "ab726555a9a72e6dc80649809147823a813fa95b",
         "type": "github"
       },
       "original": {
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "a35a6144b976f70827c2fe2f5c89d16d8f9179d8",
+        "rev": "ab726555a9a72e6dc80649809147823a813fa95b",
         "type": "github"
       }
     },
diff --git a/libcrux-Cargo.lock b/libcrux-Cargo.lock
index e6c3617a..23d51fdd 100644
--- a/libcrux-Cargo.lock
+++ b/libcrux-Cargo.lock
@@ -381,15 +381,6 @@ version = "1.0.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "b05b61dc5112cbb17e4b6cd61790d9845d13888356391624cbe7e41efeac1e75"
 
-[[package]]
-name = "combined_extraction"
-version = "0.0.2"
-dependencies = [
- "libcrux-ml-dsa",
- "libcrux-ml-kem",
- "libcrux-sha3",
-]
-
 [[package]]
 name = "const-oid"
 version = "0.9.6"
diff --git a/out/test-libcrux/internal/libcrux_mlkem_portable.h b/out/test-libcrux/internal/libcrux_mlkem_portable.h
index 1ae14859..7813ada4 100644
--- a/out/test-libcrux/internal/libcrux_mlkem_portable.h
+++ b/out/test-libcrux/internal/libcrux_mlkem_portable.h
@@ -579,7 +579,7 @@ A monomorphic instance of libcrux_ml_kem.hash_functions.portable.shake128_init_a
 with const generics
 - K= 2
 */
-Eurydice_arr_730
+Eurydice_arr_73
 libcrux_ml_kem_hash_functions_portable_shake128_init_absorb_final_4a_fd(
   const Eurydice_arr_f9 *input
 );
@@ -594,7 +594,7 @@ with const generics
 */
 Eurydice_arr_31
 libcrux_ml_kem_hash_functions_portable_shake128_squeeze_first_three_blocks_4a_fd(
-  Eurydice_arr_730 *self
+  Eurydice_arr_73 *self
 );
 
 /**
@@ -606,9 +606,7 @@ with const generics
 - K= 2
 */
 Eurydice_arr_dc0
-libcrux_ml_kem_hash_functions_portable_shake128_squeeze_next_block_4a_fd(
-  Eurydice_arr_730 *self
-);
+libcrux_ml_kem_hash_functions_portable_shake128_squeeze_next_block_4a_fd(Eurydice_arr_73 *self);
 
 /**
  Generate an unpacked key from a serialized key.
diff --git a/out/test-libcrux/libcrux_mlkem_avx2.c b/out/test-libcrux/libcrux_mlkem_avx2.c
index 1eaf9681..1a1e2c9e 100644
--- a/out/test-libcrux/libcrux_mlkem_avx2.c
+++ b/out/test-libcrux/libcrux_mlkem_avx2.c
@@ -10019,7 +10019,7 @@ static KRML_MUSTINLINE Eurydice_arr_d3 sample_from_xof_b3(const Eurydice_arr_f9
 {
   Eurydice_arr_fb sampled_coefficients = { .data = { 0U } };
   Eurydice_arr_d6 out = { .data = { { .data = { 0U } }, { .data = { 0U } } } };
-  Eurydice_arr_730
+  Eurydice_arr_73
   xof_state = libcrux_ml_kem_hash_functions_portable_shake128_init_absorb_final_4a_fd(seeds);
   Eurydice_arr_31
   randomness0 =
diff --git a/out/test-libcrux/libcrux_mlkem_portable.c b/out/test-libcrux/libcrux_mlkem_portable.c
index 5d9a0feb..f32dcae6 100644
--- a/out/test-libcrux/libcrux_mlkem_portable.c
+++ b/out/test-libcrux/libcrux_mlkem_portable.c
@@ -6221,9 +6221,9 @@ A monomorphic instance of libcrux_ml_kem.hash_functions.portable.shake128_init_a
 with const generics
 - K= 2
 */
-static inline Eurydice_arr_730 shake128_init_absorb_final_fd(const Eurydice_arr_f9 *input)
+static inline Eurydice_arr_73 shake128_init_absorb_final_fd(const Eurydice_arr_f9 *input)
 {
-  Eurydice_arr_730 shake128_state;
+  Eurydice_arr_73 shake128_state;
   Eurydice_arr_26 repeat_expression[2U];
   KRML_MAYBE_FOR2(i,
     (size_t)0U,
@@ -6249,7 +6249,7 @@ A monomorphic instance of libcrux_ml_kem.hash_functions.portable.shake128_init_a
 with const generics
 - K= 2
 */
-Eurydice_arr_730
+Eurydice_arr_73
 libcrux_ml_kem_hash_functions_portable_shake128_init_absorb_final_4a_fd(
   const Eurydice_arr_f9 *input
 )
@@ -6262,7 +6262,7 @@ A monomorphic instance of libcrux_ml_kem.hash_functions.portable.shake128_squeez
 with const generics
 - K= 2
 */
-static inline Eurydice_arr_31 shake128_squeeze_first_three_blocks_fd(Eurydice_arr_730 *st)
+static inline Eurydice_arr_31 shake128_squeeze_first_three_blocks_fd(Eurydice_arr_73 *st)
 {
   Eurydice_arr_31 out = { .data = { { .data = { 0U } }, { .data = { 0U } } } };
   KRML_MAYBE_FOR2(i,
@@ -6285,7 +6285,7 @@ with const generics
 */
 Eurydice_arr_31
 libcrux_ml_kem_hash_functions_portable_shake128_squeeze_first_three_blocks_4a_fd(
-  Eurydice_arr_730 *self
+  Eurydice_arr_73 *self
 )
 {
   return shake128_squeeze_first_three_blocks_fd(self);
@@ -6397,7 +6397,7 @@ A monomorphic instance of libcrux_ml_kem.hash_functions.portable.shake128_squeez
 with const generics
 - K= 2
 */
-static inline Eurydice_arr_dc0 shake128_squeeze_next_block_fd(Eurydice_arr_730 *st)
+static inline Eurydice_arr_dc0 shake128_squeeze_next_block_fd(Eurydice_arr_73 *st)
 {
   Eurydice_arr_dc0 out = { .data = { { .data = { 0U } }, { .data = { 0U } } } };
   KRML_MAYBE_FOR2(i,
@@ -6419,9 +6419,7 @@ with const generics
 - K= 2
 */
 Eurydice_arr_dc0
-libcrux_ml_kem_hash_functions_portable_shake128_squeeze_next_block_4a_fd(
-  Eurydice_arr_730 *self
-)
+libcrux_ml_kem_hash_functions_portable_shake128_squeeze_next_block_4a_fd(Eurydice_arr_73 *self)
 {
   return shake128_squeeze_next_block_fd(self);
 }
@@ -6554,7 +6552,7 @@ static KRML_MUSTINLINE Eurydice_arr_3d0 sample_from_xof_2b0(const Eurydice_arr_f
 {
   Eurydice_arr_fb sampled_coefficients = { .data = { 0U } };
   Eurydice_arr_d6 out = { .data = { { .data = { 0U } }, { .data = { 0U } } } };
-  Eurydice_arr_730
+  Eurydice_arr_73
   xof_state = libcrux_ml_kem_hash_functions_portable_shake128_init_absorb_final_4a_fd(seeds);
   Eurydice_arr_31
   randomness0 =
diff --git a/out/test-libcrux/libcrux_sha3_portable.h b/out/test-libcrux/libcrux_sha3_portable.h
index 72eff6a8..7db9e271 100644
--- a/out/test-libcrux/libcrux_sha3_portable.h
+++ b/out/test-libcrux/libcrux_sha3_portable.h
@@ -1927,7 +1927,7 @@ with types libcrux_sha3_portable_KeccakState
 with const generics
 - $2size_t
 */
-typedef struct Eurydice_arr_730_s { Eurydice_arr_26 data[2U]; } Eurydice_arr_730;
+typedef struct Eurydice_arr_73_s { Eurydice_arr_26 data[2U]; } Eurydice_arr_73;
 
 #if defined(__cplusplus)
 }