diff --git a/charon-pin b/charon-pin
index 94b3c0386..2b6da3a29 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.
-ac5539d88128755c32da28ed78884fe899afe452
+af5e49f331165e63ca25071f2335da38815fc1e9
diff --git a/flake.lock b/flake.lock
index 6a69fdcc7..e8d071140 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1752146446,
-        "narHash": "sha256-HYf1+RhyAucYrC4Z47y03KzcR8GQKDR+nbh4KIYLVmg=",
+        "lastModified": 1752235715,
+        "narHash": "sha256-9RXJKoO+WYdCaFzMWvqeore6f8lcedfpSGh0ey6UTD0=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "ac5539d88128755c32da28ed78884fe899afe452",
+        "rev": "af5e49f331165e63ca25071f2335da38815fc1e9",
         "type": "github"
       },
       "original": {
diff --git a/src/interp/InterpreterBorrowsCore.ml b/src/interp/InterpreterBorrowsCore.ml
index ff3fa52b2..fc6882dde 100644
--- a/src/interp/InterpreterBorrowsCore.ml
+++ b/src/interp/InterpreterBorrowsCore.ml
@@ -1467,7 +1467,6 @@ let rec norm_proj_tys_union (span : Meta.span) (ty1 : rty) (ty2 : rty) : rty =
   | TTraitType (tr1, item1), TTraitType (tr2, item2) ->
       sanity_check __FILE__ __LINE__ (item1 = item2) span;
       TTraitType (norm_proj_trait_refs_union span tr1 tr2, item1)
-  | TDynTrait (), TDynTrait () -> TDynTrait ()
   | ( TFnPtr
         { binder_regions = binder_regions1; binder_value = inputs1, output1 },
       TFnPtr
diff --git a/src/llbc/Contexts.ml b/src/llbc/Contexts.ml
index 7337fd136..9c99d4a06 100644
--- a/src/llbc/Contexts.ml
+++ b/src/llbc/Contexts.ml
@@ -7,13 +7,13 @@ open ValuesUtils
 open Errors
 include ContextsBase
 
-module OrderedBinder : Collections.OrderedType with type t = binder = struct
-  type t = binder
+module OrderedBinder : Collections.OrderedType with type t = var_binder = struct
+  type t = var_binder
 
-  let compare x y = compare_binder x y
-  let to_string x = show_binder x
-  let pp_t fmt x = Format.pp_print_string fmt (show_binder x)
-  let show_t x = show_binder x
+  let compare x y = compare_var_binder x y
+  let to_string x = show_var_binder x
+  let pp_t fmt x = Format.pp_print_string fmt (show_var_binder x)
+  let show_t x = show_var_binder x
 end
 
 module BinderMap = Collections.MakeMap (OrderedBinder)
@@ -104,7 +104,7 @@ let lookup_const_generic_var (ctx : eval_ctx) (vid : ConstGenericVarId.id) :
 
 (** Lookup a variable in the current frame *)
 let env_lookup_var (span : Meta.span) (env : env) (vid : LocalId.id) :
-    var_binder * typed_value =
+    real_var_binder * typed_value =
   (* We take care to stop at the end of current frame: different variables
      in different frames can have the same id!
   *)
@@ -120,8 +120,8 @@ let env_lookup_var (span : Meta.span) (env : env) (vid : LocalId.id) :
   in
   lookup env
 
-let ctx_lookup_var_binder (span : Meta.span) (ctx : eval_ctx) (vid : LocalId.id)
-    : var_binder =
+let ctx_lookup_real_var_binder (span : Meta.span) (ctx : eval_ctx)
+    (vid : LocalId.id) : real_var_binder =
   fst (env_lookup_var span ctx.env vid)
 
 let ctx_lookup_type_decl (span : Meta.span) (ctx : eval_ctx)
@@ -183,7 +183,7 @@ let env_update_var_value (span : Meta.span) (env : env) (vid : LocalId.id)
   in
   update env
 
-let var_to_binder (var : local) : var_binder =
+let var_to_binder (var : local) : real_var_binder =
   { index = var.index; name = var.name }
 
 (** Update a variable's value in an evaluation context.
diff --git a/src/llbc/ContextsBase.ml b/src/llbc/ContextsBase.ml
index 4b6173c2c..9e9e4454c 100644
--- a/src/llbc/ContextsBase.ml
+++ b/src/llbc/ContextsBase.ml
@@ -139,18 +139,18 @@ class ['self] map_env_base =
   end
 
 (** A binder used in an environment, to map a variable to a value *)
-type var_binder = {
+type real_var_binder = {
   index : local_id;  (** Unique variable identifier *)
   name : string option;  (** Possible name *)
 }
 
 (** A binder, for a "real" variable or a dummy variable *)
-and binder = BVar of var_binder | BDummy of dummy_var_id
+and var_binder = BVar of real_var_binder | BDummy of dummy_var_id
 
 (** Environment value: mapping from variable to value, abstraction (only used in
     symbolic mode) or stack frame delimiter. *)
 and env_elem =
-  | EBinding of binder * typed_value
+  | EBinding of var_binder * typed_value
       (** Variable binding - the binder is None if the variable is a dummy
           variable (we use dummy variables to store temporaries while doing
           bookkeeping such as ending borrows for instance). *)
diff --git a/src/llbc/Print.ml b/src/llbc/Print.ml
index 7bda206c7..c85a660a8 100644
--- a/src/llbc/Print.ml
+++ b/src/llbc/Print.ml
@@ -419,7 +419,8 @@ end
 module Contexts = struct
   open Values
 
-  let var_binder_to_string (env : fmt_env) (bv : var_binder) : string =
+  let real_var_binder_to_string (env : fmt_env) (bv : real_var_binder) : string
+      =
     match bv.name with
     | None -> local_id_to_string env bv.index
     | Some name -> name ^ "^" ^ LocalId.to_string bv.index
@@ -427,9 +428,9 @@ module Contexts = struct
   let dummy_var_id_to_string (bid : DummyVarId.id) : string =
     "_@" ^ DummyVarId.to_string bid
 
-  let binder_to_string (env : fmt_env) (bv : binder) : string =
+  let var_binder_to_string (env : fmt_env) (bv : var_binder) : string =
     match bv with
-    | BVar b -> var_binder_to_string env b
+    | BVar b -> real_var_binder_to_string env b
     | BDummy bid -> dummy_var_id_to_string bid
 
   let env_elem_to_string ?(span : Meta.span option = None) (env : fmt_env)
@@ -437,7 +438,7 @@ module Contexts = struct
       (indent_incr : string) (ev : env_elem) : string =
     match ev with
     | EBinding (var, tv) ->
-        let bv = binder_to_string env var in
+        let bv = var_binder_to_string env var in
         let ty =
           if with_var_types then " : " ^ ty_to_string env tv.ty else ""
         in
diff --git a/src/symbolic/SymbolicAst.ml b/src/symbolic/SymbolicAst.ml
index 14e8f9394..6b43c1d6f 100644
--- a/src/symbolic/SymbolicAst.ml
+++ b/src/symbolic/SymbolicAst.ml
@@ -16,7 +16,7 @@ open LlbcAst
     information, etc.). We later use this place information to generate
     meaningful name, to prettify the generated code. *)
 type mplace =
-  | PlaceLocal of Contexts.var_binder
+  | PlaceLocal of Contexts.real_var_binder
       (** It is important that we store the binder, and not just the variable
           id, because the most important information in a place is the name of
           the variable! *)
@@ -90,7 +90,6 @@ class ['self] iter_expression_base =
 
     method visit_mplace : 'env -> mplace -> unit = fun _ _ -> ()
     method visit_espan : 'env -> espan -> unit = fun _ _ -> ()
-    method visit_span : 'env -> Meta.span -> unit = fun _ _ -> ()
 
     method visit_region_group_id_map :
         'a. ('env -> 'a -> unit) -> 'env -> 'a region_group_id_map -> unit =
diff --git a/src/symbolic/SynthesizeSymbolic.ml b/src/symbolic/SynthesizeSymbolic.ml
index 9e92a9fbf..2df402996 100644
--- a/src/symbolic/SynthesizeSymbolic.ml
+++ b/src/symbolic/SynthesizeSymbolic.ml
@@ -11,7 +11,7 @@ let mk_mplace (span : Meta.span) (p : place) (ctx : Contexts.eval_ctx) : mplace
   let rec place_to_mplace (place : place) : mplace =
     match place.kind with
     | PlaceLocal var_id ->
-        PlaceLocal (Contexts.ctx_lookup_var_binder span ctx var_id)
+        PlaceLocal (Contexts.ctx_lookup_real_var_binder span ctx var_id)
     | PlaceProjection (subplace, pe) ->
         PlaceProjection (place_to_mplace subplace, pe)
   in