diff --git a/charon-pin b/charon-pin
index c2d807dd0..956e69b6d 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.
-9f447cddf5ceaf5065f12e4a5c233ec497452005
+377317d6b25702c46ffff072fa00a3e32095e46f
diff --git a/flake.lock b/flake.lock
index b525a30b1..741d49603 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1764352175,
-        "narHash": "sha256-0pXCXAlI/qTnyoEECpLLu5ZlUqRm6Ap6Ew8YNcDSexg=",
+        "lastModified": 1764614553,
+        "narHash": "sha256-OFY2wVBn8UB0JPDUN7AsCpPipOSrS9T7NBD0MaCaX9Q=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "9f447cddf5ceaf5065f12e4a5c233ec497452005",
+        "rev": "377317d6b25702c46ffff072fa00a3e32095e46f",
         "type": "github"
       },
       "original": {
diff --git a/src/interp/InterpStatements.ml b/src/interp/InterpStatements.ml
index 52bcb0b1f..a0fc614ea 100644
--- a/src/interp/InterpStatements.ml
+++ b/src/interp/InterpStatements.ml
@@ -411,9 +411,9 @@ let eval_builtin_function_call_concrete (config : config) (span : Meta.span)
   let args = call.args in
   let dest = call.dest in
   match call.func with
-  | FnOpMove _ ->
-      (* Closure case: TODO *)
-      [%craise] span "Closures are not supported yet"
+  | FnOpDynamic _ ->
+      (* Function pointer case: TODO *)
+      [%craise] span "Function pointers are not supported yet"
   | FnOpRegular func ->
       let generics = func.generics in
       (* Sanity check: we don't fully handle the const generic vars environment
@@ -613,9 +613,9 @@ let eval_non_builtin_function_call_symbolic_inst (span : Meta.span)
     (call : call) (ctx : eval_ctx) :
     fn_ptr_kind * generic_args * fun_decl * inst_fun_sig =
   match call.func with
-  | FnOpMove _ ->
-      (* Closure case: TODO *)
-      [%craise] span "Closures are not supported yet"
+  | FnOpDynamic _ ->
+      (* Function pointer case: TODO *)
+      [%craise] span "Function pointers are not supported yet"
   | FnOpRegular func ->
       let fid, generics, tr_self =
         match func.kind with
@@ -1257,7 +1257,7 @@ and eval_function_call_concrete (config : config) (span : Meta.span)
     (call : call) : stl_cm_fun =
  fun ctx ->
   match call.func with
-  | FnOpMove _ -> [%craise] span "Closures are not supported yet"
+  | FnOpDynamic _ -> [%craise] span "Function pointers are not supported yet"
   | FnOpRegular func -> (
       match func.kind with
       | FunId (FRegular fid) ->
@@ -1276,7 +1276,7 @@ and eval_function_call_concrete (config : config) (span : Meta.span)
 and eval_function_call_symbolic (config : config) (span : Meta.span)
     (call : call) : stl_cm_fun =
   match call.func with
-  | FnOpMove _ -> [%craise] span "Closures are not supported yet"
+  | FnOpDynamic _ -> [%craise] span "Function pointers are not supported yet"
   | FnOpRegular func -> (
       match func.kind with
       | FunId (FRegular _) | TraitMethod _ ->
@@ -1292,7 +1292,7 @@ and eval_non_builtin_function_call_concrete (config : config) (span : Meta.span)
   let args = call.args in
   let dest = call.dest in
   match call.func with
-  | FnOpMove _ -> [%craise] span "Closures are not supported yet"
+  | FnOpDynamic _ -> [%craise] span "Function pointers are not supported yet"
   | FnOpRegular func ->
       let generics = func.generics in
       (* Sanity check: we don't fully handle the const generic vars environment
diff --git a/src/llbc/FunsAnalysis.ml b/src/llbc/FunsAnalysis.ml
index 35cf702c6..65836d9f0 100644
--- a/src/llbc/FunsAnalysis.ml
+++ b/src/llbc/FunsAnalysis.ml
@@ -124,7 +124,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) :
 
           method! visit_Call env call =
             (match call.func with
-            | FnOpMove _ ->
+            | FnOpDynamic _ ->
                 (* Ignoring this: we lookup the called function upon creating
                    the closure *)
                 ()