diff --git a/bin/main.ml b/bin/main.ml
index 97557ea..021e8ef 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -127,8 +127,10 @@ Supported options:|}
   let files = Krml.Simplify.fixup_hoist#visit_files () files in
   let files = Krml.Simplify.misc_cosmetic#visit_files () files in
   let files = Krml.Simplify.let_to_sequence#visit_files () files in
+  Eurydice.Logging.log "Phase2.5" "%a" pfiles files;
   let files = Krml.Inlining.cross_call_analysis files in
   let files = Krml.Simplify.remove_unused files in
+  (* Macros stemming from globals *)
   let files, macros = Eurydice.Cleanup2.build_macros files in
 
   Eurydice.Logging.log "Phase3" "%a" pfiles files;
@@ -136,24 +138,16 @@ Supported options:|}
   if errors then
     exit 1;
 
+  let scope_env = Krml.Simplify.allocate_c_env files in
+  let files = Eurydice.Cleanup3.decay_cg_externals#visit_files (scope_env, false) files in
   let macros =
-    Krml.Idents.LidSet.union
-      macros
-      ((object(self)
-        inherit [_] Krml.Ast.reduce
-        method private zero = Krml.Idents.LidSet.empty
-        method private plus = Krml.Idents.LidSet.union
-        method! visit_DExternal _ _ _ n_cgs n name _ _ =
-          if n > 0 || n_cgs > 0 then
-            Krml.Idents.LidSet.singleton name
-          else
-            self#zero
-      end)#visit_files () files)
+    let cg_macros = Eurydice.Cleanup3.build_cg_macros#visit_files () files in
+    Krml.Idents.LidSet.(union (union macros cg_macros) Eurydice.Builtin.macros)
   in
-  let macros = Krml.Idents.LidSet.union macros Eurydice.Builtin.macros in
+  let c_name_map = Krml.GlobalNames.mapping (fst scope_env) in
+
   let open Krml in
   let file_of_map = Bundle.mk_file_of files in
-  let c_name_map = Simplify.allocate_c_names files in
   let deps = Bundles.direct_dependencies_with_internal files file_of_map in
   let files = List.map (fun (f, ds) ->
     let is_fine = function
diff --git a/flake.lock b/flake.lock
index e5680b0..d07613e 100644
--- a/flake.lock
+++ b/flake.lock
@@ -167,11 +167,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1707785177,
-        "narHash": "sha256-DPUINtVtpTiK5fb01JKv6pFR28QCUsyzf47OegGrg7s=",
+        "lastModified": 1707954613,
+        "narHash": "sha256-UVixnlHYQYicZOpr9iQm47aFmsaMGFpG/q3L8sRuwck=",
         "owner": "FStarLang",
         "repo": "karamel",
-        "rev": "7cf2361746b4c26877bd7f1a2c48ffb889eeab12",
+        "rev": "08bfa78ae1df5639446e6c5897b07c9823fbf3b0",
         "type": "github"
       },
       "original": {
diff --git a/lib/Bundles.ml b/lib/Bundles.ml
index cd844fd..a5fe7e7 100644
--- a/lib/Bundles.ml
+++ b/lib/Bundles.ml
@@ -18,7 +18,6 @@ type config = file list
 let load_config (path: string): Yaml.value =
   (* TODO: library not found: Yaml_unix *)
   let contents = Krml.Utils.file_get_contents path in
-  print_endline contents;
   match Yaml.of_string contents with
   | Error (`Msg s) ->
       Krml.Warn.fatal_error "Issue reading configuration file: %s" s
@@ -64,8 +63,21 @@ let parse_file (v: Yaml.value): file =
         | Some (`A private_) -> List.map parse_pattern private_
         | Some _ -> parsing_error "private not a list"
       in
+      let include_ =
+        match lookup "include_in_h" with
+        | None -> []
+        | Some (`A include_) -> List.map (function `String s -> Krml.Options.HeaderOnly name, s | _ -> parsing_error "include_in_h must be a string") include_
+        | Some _ -> parsing_error "include_in_h must be a list"
+      in
+      let c_include_ =
+        match lookup "include_in_c" with
+        | None -> []
+        | Some (`A include_) -> List.map (function `String s -> Krml.Options.COnly name, s | _ -> parsing_error "include_in_c must be a string") include_
+        | Some _ -> parsing_error "include_in_c must be a list"
+      in
       if !count < List.length ls then
         parsing_error "extraneous fields in file";
+      Krml.Options.(add_include := include_ @ c_include_ @ !add_include);
       { name; api; private_ }
   | _ ->
       parsing_error "file must be an object"
@@ -115,11 +127,11 @@ let bundle (files: file list) (c: config): files =
             false
         | { name; api; private_ } :: files ->
             if List.exists (matches lid) api then begin
-              Krml.(KPrint.bprintf "%a goes (api) into %s\n" PrintAst.Ops.plid lid name);
+              (* Krml.(KPrint.bprintf "%a goes (api) into %s\n" PrintAst.Ops.plid lid name); *)
               bundle name decl;
               true
             end else if List.exists (matches lid) private_ then begin
-              Krml.(KPrint.bprintf "%a goes (private) into %s\n" PrintAst.Ops.plid lid name);
+              (* Krml.(KPrint.bprintf "%a goes (private) into %s\n" PrintAst.Ops.plid lid name); *)
               bundle name (Krml.Bundles.mark_private decl);
               true
             end else
diff --git a/lib/Cleanup3.ml b/lib/Cleanup3.ml
new file mode 100644
index 0000000..7229e73
--- /dev/null
+++ b/lib/Cleanup3.ml
@@ -0,0 +1,84 @@
+(* Administrative cleanups that do not get checked. *)
+
+(* CG-polymorphic external signatures generally cannot be implemented with C functions, and Eurydice
+   expects those to be hand-written using macros. There is one exception, though:
+   - all of the const generics appear in positions that would anyhow decay to pointers (e.g.,
+     void f<N>(int x[N]) can be replaced by void f(int *x) -- it's the same in C)
+   - the return type is unit -- the implementation doesn't need to receive the return type as an
+     argument
+*)
+
+open Krml
+open Ast
+
+let decay_cg_externals = object(self)
+  inherit [_] Krml.Ast.map as super
+
+  (* Since we allocate new names, we reuse the C name allocation facility *)
+  inherit Simplify.scope_helpers
+
+  method! visit_file env f =
+    current_file <- fst f;
+    super#visit_file env f
+
+  method! visit_TCgArray (env, under_external) t n =
+    if under_external then
+      raise Exit
+    else
+      super#visit_TCgArray (env, under_external) t n
+
+  method! visit_TCgApp (env, under_external) t n =
+    if under_external then
+      raise Exit
+    else
+      super#visit_TCgApp (env, under_external) t n
+
+  method! visit_DExternal (scope_env, _) cc flags n_cgs n name t hints =
+    let t_ret, t_args = Helpers.flatten_arrow t in
+    if t_ret = TUnit && n_cgs > 0 then
+      let t_args = List.map (function
+        | TCgArray (t, _) -> TBuf (t, false)
+        | t -> t
+      ) t_args in
+      try
+        (* This throws and aborts if there are some const generics left. *)
+        let t_args = List.map (self#visit_typ (scope_env, true)) t_args in
+
+        (* We're good. Find the allocated C name for our declaration, and allocate a new C name for
+           the extra declaration *)
+        let c_name = Option.get (GlobalNames.lookup (fst scope_env) name) in
+        let new_name = fst name, snd name ^ "_" in
+        self#record scope_env ~is_type:false ~is_external:true flags new_name;
+        let new_c_name = Option.get (GlobalNames.lookup (fst scope_env) new_name) in
+
+        (* We build: #define <<c_name>>(x0, ..., xn, _ret_t) \
+           <<new_c_name>>(x0, ..., xn) *)
+        let prelude =
+          (* Names of the arguments *)
+          let names =
+            if List.length hints = List.length t_args then
+              hints
+            else
+              List.init (List.length t_args) (fun i -> KPrint.bsprintf "x_%d" i)
+          in
+          KPrint.bsprintf "#define %s(%s) %s(%s)"
+            c_name (String.concat ", " (names @ [ "_ret_t" ]))
+            new_c_name (String.concat ", " names)
+        in
+        DExternal (cc, [ Common.Prologue prelude ] @ flags, 0, n, new_name, Helpers.fold_arrow t_args t_ret, hints)
+      with Exit ->
+        DExternal (cc, flags, n_cgs, n, name, t, hints)
+    else
+      DExternal (cc, flags, n_cgs, n, name, t, hints)
+end
+
+let build_cg_macros = object(self)
+  inherit [_] Krml.Ast.reduce
+  method private zero = Krml.Idents.LidSet.empty
+  method private plus = Krml.Idents.LidSet.union
+  method! visit_DExternal () _ _ n_cgs n name _ _ =
+    if n > 0 || n_cgs > 0 then
+      Krml.Idents.LidSet.singleton name
+    else
+      self#zero
+end