diff --git a/lib/AstToCFlat.ml b/lib/AstToCFlat.ml
index 85f360578..40fc613ca 100644
--- a/lib/AstToCFlat.ml
+++ b/lib/AstToCFlat.ml
@@ -67,7 +67,7 @@ type env = {
      *     StringLiteral. The strings are shared in memory at compile-time, and
      *     hashconsing in CFlatToWasm guarantees that they are shared in the
      *     resulting code, too. *)
-  names: (lident, ident) Hashtbl.t;
+  names: GlobalNames.mapping;
 }
 
 
diff --git a/lib/AstToCStar.ml b/lib/AstToCStar.ml
index e472a79ee..4c55cf04e 100644
--- a/lib/AstToCStar.ml
+++ b/lib/AstToCStar.ml
@@ -975,7 +975,7 @@ and mk_files files m ifdefs macros =
 let mk_macros_set files =
   let seen = Hashtbl.create 31 in
   let record x =
-    let t = String.uppercase_ascii GlobalNames.(target_c_name ~attempt_shortening:false ~kind:Macro x) in
+    let t = fst GlobalNames.(target_c_name ~attempt_shortening:false ~kind:Macro x) in
     if Hashtbl.mem seen t then
       Warn.(maybe_fatal_error ("", ConflictMacro (x, t)));
     Hashtbl.add seen t ()
diff --git a/lib/CStarToC11.ml b/lib/CStarToC11.ml
index 4c23e01b0..385e6f2ec 100644
--- a/lib/CStarToC11.ml
+++ b/lib/CStarToC11.ml
@@ -64,10 +64,9 @@ module S = Set.Make(String)
 let rec vars_of m = function
   | CStar.Var v ->
       S.singleton v
-  | Qualified v ->
-      S.singleton (to_c_name m v)
+  | Qualified v
   | Macro v ->
-      S.singleton (String.uppercase_ascii (to_c_name m v))
+      S.singleton (to_c_name m v)
   | Constant _
   | Bool _
   | StringLiteral _
@@ -935,11 +934,9 @@ and mk_expr m (e: expr): C.expr =
   | Var ident ->
       Name ident
 
-  | Qualified ident ->
-      Name (to_c_name m ident)
-
+  | Qualified ident
   | Macro ident ->
-      Name (String.uppercase_ascii (to_c_name m ident))
+      Name (to_c_name m ident)
 
   | Constant (w, c) ->
       (* See discussion in AstToCStar.ml, around mk_arith. *)
@@ -1338,7 +1335,7 @@ let mk_file m decls =
         (if_private_or_abstract_struct (mk_type_or_external m C))))
     decls
 
-let mk_files (map: (Ast.lident, Ast.ident) Hashtbl.t) files =
+let mk_files (map: GlobalNames.mapping) files =
   List.map (fun (name, program) -> name, mk_file map program) files
 
 (* Building three flavors of headers. *)
@@ -1368,7 +1365,7 @@ let mk_static f d =
 
 (* Generates either a static header (the union of public + internal), OR just
    the public part. *)
-let mk_public_header (m: (Ast.lident, Ast.ident) Hashtbl.t) decls =
+let mk_public_header (m: GlobalNames.mapping) decls =
   (* In the header file, we put functions and global stubs, along with type
    * definitions that are visible from the outside. *)
   (* What should be the behavior for a type declaration marked as CAbstract but
@@ -1384,7 +1381,7 @@ let mk_public_header (m: (Ast.lident, Ast.ident) Hashtbl.t) decls =
     decls
 
 (* Private part if not already a static header, empty otherwise. *)
-let mk_internal_header (m: (Ast.lident, Ast.ident) Hashtbl.t) decls =
+let mk_internal_header (m: GlobalNames.mapping) decls =
   KList.map_flatten
     (if_internal (
       (if_header_inline_static m
@@ -1392,7 +1389,7 @@ let mk_internal_header (m: (Ast.lident, Ast.ident) Hashtbl.t) decls =
         (either (mk_function_or_global_stub m) (mk_type_or_external m H)))))
     decls
 
-let mk_headers (map: (Ast.lident, Ast.ident) Hashtbl.t)
+let mk_headers (map: GlobalNames.mapping)
   (files: (string * CStar.decl list) list)
 =
   (* Generate headers with a sensible order for the message "WRITING H FILES: ...". *)
diff --git a/lib/GenCtypes.ml b/lib/GenCtypes.ml
index 35126faa8..e319ad859 100644
--- a/lib/GenCtypes.ml
+++ b/lib/GenCtypes.ml
@@ -351,7 +351,7 @@ type t =
  * OCaml declarations. *)
 let mk_ocaml_bindings
   (files : (ident * decl list) list)
-  (m: (A.lident, A.ident) Hashtbl.t)
+  (m: GlobalNames.mapping)
   (file_of: A.lident -> string option):
   (string * string list * structure_item list) list
 =
diff --git a/lib/GenCtypes.mli b/lib/GenCtypes.mli
index 00e0d474e..dbfcea177 100644
--- a/lib/GenCtypes.mli
+++ b/lib/GenCtypes.mli
@@ -2,7 +2,7 @@ type t
 
 val mk_ocaml_bindings:
   (CStar.ident * CStar.decl list) list ->
-  (Ast.lident, Ast.ident) Hashtbl.t ->
+  GlobalNames.mapping ->
   (Ast.lident -> string option) ->
   t
 
diff --git a/lib/GlobalNames.ml b/lib/GlobalNames.ml
index 8c545051c..6eddd2a81 100644
--- a/lib/GlobalNames.ml
+++ b/lib/GlobalNames.ml
@@ -8,12 +8,12 @@ open Idents
 open Ast
 open PrintAst.Ops
 
-type mapping = (lident, string) Hashtbl.t
+type mapping = (lident, string * bool) Hashtbl.t
 type t = mapping * (string, unit) Hashtbl.t
 
 let dump (env: t) =
-  Hashtbl.iter (fun lident c_name ->
-    KPrint.bprintf "%a --> %s\n" plid lident c_name
+  Hashtbl.iter (fun lident (c_name, nm) ->
+    KPrint.bprintf "%a --> %s%s\n" plid lident c_name (if nm then " (!)" else "")
   ) (fst env);
   Hashtbl.iter (fun c_name _ ->
     KPrint.bprintf "%s is used\n" c_name
@@ -145,7 +145,7 @@ let create () =
   reserve_keywords used_c_names;
   c_of_original, used_c_names
 
-let extend (global: t) (local: t) is_local original_name desired_name =
+let extend (global: t) (local: t) is_local original_name (desired_name, non_modular_renaming) =
   let c_of_original, g_used_c_names = global in
   let _, l_used_c_names = local in
   if Hashtbl.mem c_of_original original_name then
@@ -153,7 +153,7 @@ let extend (global: t) (local: t) is_local original_name desired_name =
 
   let unique_c_name = mk_fresh desired_name (fun x ->
     Hashtbl.mem g_used_c_names x || Hashtbl.mem l_used_c_names x) in
-  Hashtbl.add c_of_original original_name unique_c_name;
+  Hashtbl.add c_of_original original_name (unique_c_name, non_modular_renaming && not is_local);
   if is_local then
     Hashtbl.add l_used_c_names unique_c_name ()
   else
@@ -162,7 +162,7 @@ let extend (global: t) (local: t) is_local original_name desired_name =
 
 let lookup (env: t) name =
   let c_of_original, _ = env in
-  Hashtbl.find_opt c_of_original name
+  Option.map fst (Hashtbl.find_opt c_of_original name)
 
 let clone (env: t) =
   let c_of_original, used_c_names = env in
@@ -221,12 +221,12 @@ let pascal_case name =
     done;
     Buffer.contents b
   else
-    String.uppercase_ascii (String.sub name 0 1) ^ 
+    String.uppercase_ascii (String.sub name 0 1) ^
     String.sub name 1 (String.length name - 1)
 
 let camel_case name =
   let name = pascal_case name in
-  String.lowercase_ascii (String.sub name 0 1) ^ 
+  String.lowercase_ascii (String.sub name 0 1) ^
   String.sub name 1 (String.length name - 1)
 
 let strip_leading_underscores name =
@@ -238,37 +238,48 @@ let strip_leading_underscores name =
 
 type kind = Macro | Type | Other
 
+(* Clients feed the result of this to extend -- this is a tentative name that
+   may still generate a collision. *)
 let target_c_name ~attempt_shortening ?(kind=Other) lid =
-  let pre_name =
+  (* A non-modular renaming is one that is influenced by command-line
+     options (e.g. -no-prefix, -bundle ...[rename-prefix], etc.). Such name
+     choices pose difficulties in the verified library + verified client
+     scenario, because the client needs to replicate the same options in order
+     to be able to link against the library. *)
+  let pre_name, non_modular_renaming =
     if skip_prefix lid && not (ineligible lid) then
-      snd lid
+      snd lid, true
     else if attempt_shortening && !Options.short_names && not (ineligible lid) && snd lid <> "main" then
-      snd lid
+      snd lid, false
     else match rename_prefix lid with
     | Some prefix ->
-        prefix ^ "_" ^ snd lid
+        prefix ^ "_" ^ snd lid, true
     | None ->
-        string_of_lident lid
+        string_of_lident lid, false
   in
-  if !Options.microsoft then
-    if pre_name = "main" then
-      pre_name
+  let formatted_name =
+    if !Options.microsoft then
+      if pre_name = "main" then
+        pre_name
+      else
+        match kind with
+        | Other ->
+            pascal_case pre_name
+        | Macro ->
+            strip_leading_underscores pre_name
+        | Type ->
+            String.uppercase_ascii (strip_leading_underscores pre_name)
     else
-      match kind with
-      | Other ->
-          pascal_case pre_name
-      | Macro ->
-          strip_leading_underscores pre_name
-      | Type ->
-          String.uppercase_ascii (strip_leading_underscores pre_name)
-  else
-    pre_name
+      pre_name
+  in
+  let formatted_name = if kind = Macro then String.uppercase_ascii formatted_name else formatted_name in
+  formatted_name, non_modular_renaming
 
 let to_c_name ?kind m lid =
   try
-    Hashtbl.find m lid
+    fst (Hashtbl.find m lid)
   with Not_found ->
     (* Note: this happens for external types which are not retained as DType
        nodes and therefore are not recorded in the initial name-assignment
        phase. *)
-    Idents.to_c_identifier (target_c_name ?kind ~attempt_shortening:false lid)
+    Idents.to_c_identifier (fst (target_c_name ?kind ~attempt_shortening:false lid))
diff --git a/lib/GlobalNames.mli b/lib/GlobalNames.mli
index 8f65c1d76..95fcde787 100644
--- a/lib/GlobalNames.mli
+++ b/lib/GlobalNames.mli
@@ -3,7 +3,7 @@
 
 type t
 
-type mapping = (Ast.lident, Ast.ident) Hashtbl.t
+type mapping = (Ast.lident, Ast.ident * bool) Hashtbl.t
 
 (** Allocate a new (mutable) table for a given C scope of top-level declarations. *)
 val create: unit -> t
@@ -11,7 +11,7 @@ val create: unit -> t
 (** `extend t name c_name` tries to associate `c_name` to `name` in the table
  * `t`. If case there is a name conflict or `c_name` is an invalid C identifier,
  * a suitable replacement name based on `c_name` will be chosen. *)
-val extend: t -> t -> bool -> Ast.lident -> string -> string
+val extend: t -> t -> bool -> Ast.lident -> (string * bool) -> string
 
 (** `lookup t name fallback` recalls the C name associated to `name` in `t`. *)
 val lookup: t -> Ast.lident -> string option
@@ -24,7 +24,7 @@ val clone: t -> t
 
 type kind = Macro | Type | Other
 
-val target_c_name: attempt_shortening:bool -> ?kind:kind -> Ast.lident -> string
+val target_c_name: attempt_shortening:bool -> ?kind:kind -> Ast.lident -> string * bool
 
 val to_c_name: ?kind:kind -> mapping -> Ast.lident -> string
 
diff --git a/lib/Inlining.ml b/lib/Inlining.ml
index 74f23f65d..3c3ba169f 100644
--- a/lib/Inlining.ml
+++ b/lib/Inlining.ml
@@ -512,7 +512,7 @@ let cross_call_analysis files =
 (** A whole-program transformation that inlines functions according to... *)
 
 let always_live name =
-  let n = GlobalNames.target_c_name ~attempt_shortening:false name in
+  let n = fst (GlobalNames.target_c_name ~attempt_shortening:false name) in
   n = "main" ||
   String.length n >= 11 &&
   String.sub n 0 11 = "WasmSupport" &&
diff --git a/lib/Options.ml b/lib/Options.ml
index d356916e3..208d352df 100644
--- a/lib/Options.ml
+++ b/lib/Options.ml
@@ -44,6 +44,7 @@ let static_header: Bundle.pat list ref = ref []
 let minimal = ref false
 let by_ref: (string list * string) list ref = ref []
 let ctypes: Bundle.pat list ref = ref []
+let record_renamings = ref false
 
 (* wasm = true ==> these two are false *)
 let struct_passing = ref true
diff --git a/lib/Output.ml b/lib/Output.ml
index 17699d310..b5a136162 100644
--- a/lib/Output.ml
+++ b/lib/Output.ml
@@ -130,12 +130,15 @@ let write_one name prefix program suffix =
     PPrint.ToChannel.pretty 0.95 100 oc doc
   )
 
+let create_subdir d =
+  if !Options.tmpdir = "" then
+    Driver.mkdirp d
+  else
+    Driver.mkdirp (!Options.tmpdir ^ "/" ^ d)
+
 let maybe_create_internal_dir h =
   if List.exists (function (_, C11.Internal _) -> true | _ -> false) h then
-    if !Options.tmpdir = "" then
-      Driver.mkdirp "internal"
-    else
-      Driver.mkdirp (!Options.tmpdir ^ "/internal")
+    create_subdir "internal"
 
 let write_c files internal_headers deps =
   Driver.detect_fstar_if ();
@@ -227,3 +230,17 @@ let write_def m c_files =
       ) decls
     ) c_files
   )
+
+let write_renamings (m: GlobalNames.mapping) =
+  create_subdir "clients";
+  let dst = in_tmp_dir "clients/krmlrenamings.h" in
+  with_open_out_bin dst (fun oc ->
+    Hashtbl.iter (fun original_name (new_name, non_modular_renaming) ->
+      (* Note: there is a slight imprecision here. If the original name WOULD
+         HAVE BEEN renamed because of a name collision, then this renaming map
+         will be incorrect. We would to track two maps in GlobalNames, the
+         actual one, and the "sans the renamings" one, in order to be accurate.
+         Too much work, unlikely to happen. *)
+      if non_modular_renaming then
+        KPrint.bfprintf oc "#define %s %s\n" (Idents.string_of_lident original_name) new_name)
+    m)
diff --git a/lib/Simplify.ml b/lib/Simplify.ml
index 0e3e2fbb3..2b7146876 100644
--- a/lib/Simplify.ml
+++ b/lib/Simplify.ml
@@ -1965,7 +1965,7 @@ let debug env =
   ) original_of_c_name
 
 (* Allocate C names avoiding keywords and name collisions. *)
-let allocate_c_names (files: file list): (lident, ident) Hashtbl.t =
+let allocate_c_names (files: file list): GlobalNames.mapping =
   let env = GlobalNames.create (), Hashtbl.create 41 in
   record_toplevel_names#visit_files env files;
   if Options.debug "c-names" then
diff --git a/lib/Structs.ml b/lib/Structs.ml
index d4a878068..08e0c0d02 100644
--- a/lib/Structs.ml
+++ b/lib/Structs.ml
@@ -462,7 +462,7 @@ let collect_initializers (files: Ast.file list) =
       inherit [_] map
       method! visit_DFunction _ cc flags n ret name binders body =
         let body =
-          if GlobalNames.target_c_name ~attempt_shortening:false name = "main" then begin
+          if fst (GlobalNames.target_c_name ~attempt_shortening:false name) = "main" then begin
             found := true;
             with_type ret (ESequence [
               with_type TUnit (EApp (
diff --git a/src/Karamel.ml b/src/Karamel.ml
index cef3959b6..2e2436d5d 100644
--- a/src/Karamel.ml
+++ b/src/Karamel.ml
@@ -249,6 +249,9 @@ Supported options:|}
       List.iter (prepend Options.hand_written) (Parsers.drop s)),
       "  in conjunction with static-header and library";
     "-extract-uints", Arg.Set Options.extract_uints, ""; (* no doc, intentional *)
+    "-record-renamings", Arg.Set Options.record_renamings, " write a map from \
+      old names to new names in KrmlRenamings.h, useful if you're a library and \
+      don't want to impose clients to follow all of your usages of rename-prefix";
     "-header", Arg.Set_string Options.header, " prepend the contents of the given \
       file at the beginning of each .c and .h";
     "-tmpdir", Arg.Set_string Options.tmpdir, " temporary directory for .out, \
@@ -769,7 +772,11 @@ Supported options:|}
     let h_output = Output.write_h headers public_headers deps in
     GenCtypes.write_bindings ml_files;
     GenCtypes.write_gen_module ~public:public_headers ~internal:internal_headers ml_files;
-    if not !arg_skip_makefiles then Output.write_makefile user_ccopts !c_files c_output h_output;
+    if not !arg_skip_makefiles then
+      Output.write_makefile user_ccopts !c_files c_output h_output;
+    if !Options.record_renamings then
+      Output.write_renamings c_name_map;
+
     tick_print true "PrettyPrinting";
 
     if not !Options.silent then begin
diff --git a/test/sepcomp/a/Makefile b/test/sepcomp/a/Makefile
index 703e0d49f..50ac09a34 100644
--- a/test/sepcomp/a/Makefile
+++ b/test/sepcomp/a/Makefile
@@ -174,6 +174,7 @@ dist/A.h: $(filter-out %prims.krml,$(ALL_KRML_FILES))
 	$(KRML) -tmpdir $(dir $@) -skip-compilation \
 	  $(filter %.krml,$^) \
 	  -warn-error @4@5@18 \
+	  -record-renamings \
 	  -fparentheses \
 	  -static-header A.Base \
 	  -bundle 'FStar.*,LowStar.*,Prims[rename=SHOULDNOTBETHERE]' \