diff --git a/eurydice.opam b/eurydice.opam
index a040837d..38e29daf 100644
--- a/eurydice.opam
+++ b/eurydice.opam
@@ -11,7 +11,7 @@ homepage: "https://github.com/AeneasVerif/eurydice"
 bug-reports: "https://github.com/AeneasVerif/eurydice/issues"
 depends: [
   "ocaml"
-  "dune" {>= "3.7"}
+  "dune" {>= "3.13"}
   "yaml"
   "terminal" {>= "0.4.0"}
   "odoc" {with-doc}
diff --git a/flake.lock b/flake.lock
index 11dfa3ad..5c3d9955 100644
--- a/flake.lock
+++ b/flake.lock
@@ -14,11 +14,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1743077260,
-        "narHash": "sha256-CSIhHvmzDZlGrTnirgrfOehDvUsctc3qAs/IdhtdaUg=",
-        "owner": "AeneasVerif",
+        "lastModified": 1743501557,
+        "narHash": "sha256-bZZfS0bwHRQh6p3svYqVBo65xdJgVejutU1oCd2QyKM=",
+        "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "8363532b648d533ebe1d4d068d271c8b853408ca",
+        "rev": "99432e1474433e9eaed946539c12d45e72486e79",
         "type": "github"
       },
       "original": {
diff --git a/out/test-nested_arrays/nested_arrays.h b/out/test-nested_arrays/nested_arrays.h
index a3d6076b..a25ca8b8 100644
--- a/out/test-nested_arrays/nested_arrays.h
+++ b/out/test-nested_arrays/nested_arrays.h
@@ -67,7 +67,19 @@ core_iter_range___core__iter__range__Step_for_usize__43__backward_checked(size_t
 extern core_option_Option_08
 core_iter_range___core__iter__range__Step_for_usize__43__forward_checked(size_t x0, size_t x1);
 
-extern core_option_Option_08
+/**
+A monomorphic instance of K.
+with types size_t, core_option_Option size_t
+
+*/
+typedef struct tuple_04_s
+{
+  size_t fst;
+  core_option_Option_08 snd;
+}
+tuple_04;
+
+extern tuple_04
 core_iter_range___core__iter__range__Step_for_usize__43__steps_between(size_t *x0, size_t *x1);
 
 #define core_panicking_AssertKind_Eq 0
diff --git a/out/test-step_by/step_by.h b/out/test-step_by/step_by.h
index 9c17009e..1bcaa854 100644
--- a/out/test-step_by/step_by.h
+++ b/out/test-step_by/step_by.h
@@ -76,7 +76,19 @@ typedef struct core_option_Option_08_s
 }
 core_option_Option_08;
 
-extern core_option_Option_08
+/**
+A monomorphic instance of K.
+with types size_t, core_option_Option size_t
+
+*/
+typedef struct tuple_04_s
+{
+  size_t fst;
+  core_option_Option_08 snd;
+}
+tuple_04;
+
+extern tuple_04
 core_iter_range___core__iter__range__Step_for_i32__40__steps_between(int32_t *x0, int32_t *x1);
 
 #define core_panicking_AssertKind_Eq 0
diff --git a/out/test-symcrust/symcrust.h b/out/test-symcrust/symcrust.h
index 18d567a5..1a5a00c4 100644
--- a/out/test-symcrust/symcrust.h
+++ b/out/test-symcrust/symcrust.h
@@ -91,7 +91,19 @@ core_iter_range___core__iter__range__Step_for_usize__43__backward_checked(size_t
 extern core_option_Option_08
 core_iter_range___core__iter__range__Step_for_usize__43__forward_checked(size_t x0, size_t x1);
 
-extern core_option_Option_08
+/**
+A monomorphic instance of K.
+with types size_t, core_option_Option size_t
+
+*/
+typedef struct tuple_04_s
+{
+  size_t fst;
+  core_option_Option_08 snd;
+}
+tuple_04;
+
+extern tuple_04
 core_iter_range___core__iter__range__Step_for_usize__43__steps_between(size_t *x0, size_t *x1);
 
 static inline void core_num__u32_8__to_le_bytes(uint32_t x0, uint8_t x1[4U]);