diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 97db05d11..d218f4c9b 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -28,4 +28,4 @@ jobs:
       - uses: Swatinem/rust-cache@v2
 
       - name: Test
-        run: cargo test --workspace --verbose
+        run: cargo test --workspace --exclude hax-engine-names-extract --verbose
diff --git a/.utils/rebuild.sh b/.utils/rebuild.sh
index 9a58e1f2b..48e28b3b6 100755
--- a/.utils/rebuild.sh
+++ b/.utils/rebuild.sh
@@ -31,7 +31,7 @@ cd_rootwise () {
 
 rust () {
     cd_rootwise "cli"
-    for i in driver subcommands; do
+    for i in driver subcommands ../engine/names/extract; do
         CURRENT="rust/$i"
         cargo install --quiet $OFFLINE_FLAG --debug --path $i
     done
diff --git a/Cargo.lock b/Cargo.lock
index 76a4fad3b..4355800dc 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -351,12 +351,12 @@ checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5"
 
 [[package]]
 name = "errno"
-version = "0.3.5"
+version = "0.3.8"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ac3e13f66a2f95e32a39eaa81f6b95d42878ca0e1db0c7543723dfe12557e860"
+checksum = "a258e46cdc063eb8519c00b9fc845fc47bcfca4130e2f08e88665ceda8474245"
 dependencies = [
  "libc",
- "windows-sys 0.48.0",
+ "windows-sys 0.52.0",
 ]
 
 [[package]]
@@ -483,6 +483,23 @@ dependencies = [
  "which",
 ]
 
+[[package]]
+name = "hax-engine-names"
+version = "0.1.0-pre.1"
+
+[[package]]
+name = "hax-engine-names-extract"
+version = "0.1.0-pre.1"
+dependencies = [
+ "camino",
+ "cargo_metadata",
+ "hax-cli-options-engine",
+ "hax-frontend-exporter",
+ "serde",
+ "serde_json",
+ "tempfile",
+]
+
 [[package]]
 name = "hax-frontend-exporter"
 version = "0.1.0-pre.1"
@@ -686,9 +703,9 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"
 
 [[package]]
 name = "libc"
-version = "0.2.149"
+version = "0.2.152"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a08173bc88b7955d1b3145aa561539096c421ac8debde8cbc3612ec635fee29b"
+checksum = "13e3bf6590cbc649f4d1a3eefc9d5d6eb746f5200ffb04e5e142700b8faa56e7"
 
 [[package]]
 name = "libtest-mimic"
@@ -709,9 +726,9 @@ checksum = "0717cef1bc8b636c6e1c1bbdefc09e6322da8a9321966e8928ef80d20f7f770f"
 
 [[package]]
 name = "linux-raw-sys"
-version = "0.4.10"
+version = "0.4.12"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "da2479e8c062e40bf0066ffa0bc823de0a9368974af99c9f6df941d2c231e03f"
+checksum = "c4cd1a83af159aa67994778be9070f0ae1bd732942279cabb14f86f986a21456"
 
 [[package]]
 name = "lock_api"
@@ -815,7 +832,7 @@ checksum = "4c42a9226546d68acdd9c0a280d17ce19bfe27a46bf68784e4066115788d008e"
 dependencies = [
  "cfg-if",
  "libc",
- "redox_syscall 0.4.1",
+ "redox_syscall",
  "smallvec",
  "windows-targets 0.48.5",
 ]
@@ -908,15 +925,6 @@ dependencies = [
  "proc-macro2",
 ]
 
-[[package]]
-name = "redox_syscall"
-version = "0.3.5"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "567664f262709473930a4bf9e51bf2ebf3348f2e748ccc50dea20646858f8f29"
-dependencies = [
- "bitflags 1.3.2",
-]
-
 [[package]]
 name = "redox_syscall"
 version = "0.4.1"
@@ -972,15 +980,15 @@ checksum = "c08c74e62047bb2de4ff487b251e4a92e24f48745648451635cec7d591162d9f"
 
 [[package]]
 name = "rustix"
-version = "0.38.20"
+version = "0.38.28"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "67ce50cb2e16c2903e30d1cbccfd8387a74b9d4c938b6a4c5ec6cc7556f7a8a0"
+checksum = "72e572a5e8ca657d7366229cdde4bd14c4eb5499a9573d4d366fe1b599daa316"
 dependencies = [
  "bitflags 2.4.1",
  "errno",
  "libc",
  "linux-raw-sys",
- "windows-sys 0.48.0",
+ "windows-sys 0.52.0",
 ]
 
 [[package]]
@@ -1169,15 +1177,15 @@ dependencies = [
 
 [[package]]
 name = "tempfile"
-version = "3.8.0"
+version = "3.9.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "cb94d2f3cc536af71caac6b6fcebf65860b347e7ce0cc9ebe8f70d3e521054ef"
+checksum = "01ce4141aa927a6d1bd34a041795abd0db1cccba5d5f24b009f694bdf3a1f3fa"
 dependencies = [
  "cfg-if",
  "fastrand",
- "redox_syscall 0.3.5",
+ "redox_syscall",
  "rustix",
- "windows-sys 0.48.0",
+ "windows-sys 0.52.0",
 ]
 
 [[package]]
@@ -1489,6 +1497,15 @@ dependencies = [
  "windows-targets 0.48.5",
 ]
 
+[[package]]
+name = "windows-sys"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d"
+dependencies = [
+ "windows-targets 0.52.0",
+]
+
 [[package]]
 name = "windows-targets"
 version = "0.42.2"
@@ -1519,6 +1536,21 @@ dependencies = [
  "windows_x86_64_msvc 0.48.5",
 ]
 
+[[package]]
+name = "windows-targets"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8a18201040b24831fbb9e4eb208f8892e1f50a37feb53cc7ff887feb8f50e7cd"
+dependencies = [
+ "windows_aarch64_gnullvm 0.52.0",
+ "windows_aarch64_msvc 0.52.0",
+ "windows_i686_gnu 0.52.0",
+ "windows_i686_msvc 0.52.0",
+ "windows_x86_64_gnu 0.52.0",
+ "windows_x86_64_gnullvm 0.52.0",
+ "windows_x86_64_msvc 0.52.0",
+]
+
 [[package]]
 name = "windows_aarch64_gnullvm"
 version = "0.42.2"
@@ -1531,6 +1563,12 @@ version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8"
 
+[[package]]
+name = "windows_aarch64_gnullvm"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cb7764e35d4db8a7921e09562a0304bf2f93e0a51bfccee0bd0bb0b666b015ea"
+
 [[package]]
 name = "windows_aarch64_msvc"
 version = "0.42.2"
@@ -1543,6 +1581,12 @@ version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc"
 
+[[package]]
+name = "windows_aarch64_msvc"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bbaa0368d4f1d2aaefc55b6fcfee13f41544ddf36801e793edbbfd7d7df075ef"
+
 [[package]]
 name = "windows_i686_gnu"
 version = "0.42.2"
@@ -1555,6 +1599,12 @@ version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e"
 
+[[package]]
+name = "windows_i686_gnu"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a28637cb1fa3560a16915793afb20081aba2c92ee8af57b4d5f28e4b3e7df313"
+
 [[package]]
 name = "windows_i686_msvc"
 version = "0.42.2"
@@ -1567,6 +1617,12 @@ version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406"
 
+[[package]]
+name = "windows_i686_msvc"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ffe5e8e31046ce6230cc7215707b816e339ff4d4d67c65dffa206fd0f7aa7b9a"
+
 [[package]]
 name = "windows_x86_64_gnu"
 version = "0.42.2"
@@ -1579,6 +1635,12 @@ version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e"
 
+[[package]]
+name = "windows_x86_64_gnu"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3d6fa32db2bc4a2f5abeacf2b69f7992cd09dca97498da74a151a3132c26befd"
+
 [[package]]
 name = "windows_x86_64_gnullvm"
 version = "0.42.2"
@@ -1591,6 +1653,12 @@ version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc"
 
+[[package]]
+name = "windows_x86_64_gnullvm"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1a657e1e9d3f514745a572a6846d3c7aa7dbe1658c056ed9c3344c4109a6949e"
+
 [[package]]
 name = "windows_x86_64_msvc"
 version = "0.42.2"
@@ -1603,6 +1671,12 @@ version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538"
 
+[[package]]
+name = "windows_x86_64_msvc"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dff9641d1cd4be8d1a070daf9e3773c5f67e78b4d9d42263020c057706765c04"
+
 [[package]]
 name = "winnow"
 version = "0.5.17"
diff --git a/Cargo.toml b/Cargo.toml
index cb56b0837..34577906d 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -14,9 +14,29 @@ members = [
      "hax-lib-macros",
      "hax-lib-macros/types",
      "hax-lib-protocol",
-     "hax-lib-protocol-macros"
+     "hax-lib-protocol-macros",
+     "engine/names",
+     "engine/names/extract",
 ]
 exclude = ["tests"]
+default-members = [
+     "frontend/exporter",
+     "frontend/exporter/options",
+     "frontend/diagnostics",
+     "frontend/lint",
+     "cli/options",
+     "cli/options/engine",
+     "cli/subcommands",
+     "cli/driver",
+     "test-harness",
+     "engine/utils/phase-debug-webapp",
+     "hax-lib",
+     "hax-lib-macros",
+     "hax-lib-macros/types",
+     "hax-lib-protocol",
+     "hax-lib-protocol-macros",
+     "engine/names",
+]
 resolver = "2"
 
 [workspace.package]
@@ -67,3 +87,4 @@ hax-diagnostics = { path = "frontend/diagnostics", version = "=0.1.0-pre.1" }
 hax-lint = { path = "frontend/lint", version = "=0.1.0-pre.1" }
 hax-phase-debug-webapp = { path = "engine/utils/phase-debug-webapp", version = "=0.1.0-pre.1" }
 hax-lib-macros-types = { path = "hax-lib-macros/types", version = "=0.1.0-pre.1" }
+hax-engine-names = { path = "engine/names", version = "=0.1.0-pre.1" }
diff --git a/cli/default.nix b/cli/default.nix
index b03b15cd4..0805ea169 100644
--- a/cli/default.nix
+++ b/cli/default.nix
@@ -40,10 +40,13 @@
     // {
       pname = pname;
     });
-  hax = craneLib.buildPackage (commonArgs
+  hax = craneLib.buildPackage (
+    commonArgs
     // {
       inherit cargoArtifacts pname;
-    });
+      doInstallCargoArtifacts = true;
+    }
+  );
   frontend-docs = craneLib.cargoDoc (commonArgs // {inherit cargoArtifacts pname;});
   docs = stdenv.mkDerivation {
     name = "hax-docs";
@@ -103,6 +106,20 @@ in
     meta.mainProgram = "cargo-hax";
     passthru = {
       unwrapped = hax;
+      hax-engine-names-extract = craneLib.buildPackage (
+        commonArgs
+        // {
+          pname = "hax_engine_names_extract";
+          cargoLock = ../Cargo.lock;
+          cargoToml = ../engine/names/extract/Cargo.toml;
+          cargoArtifacts = hax;
+          nativeBuildInputs = [hax];
+          postUnpack = ''
+            cd $sourceRoot/engine/names/extract
+            sourceRoot="."
+          '';
+        }
+      );
       engine-docs = hax-engine.docs;
       inherit tests docs frontend-docs;
     };
diff --git a/cli/options/src/lib.rs b/cli/options/src/lib.rs
index 852ca7b0f..7f604b8bd 100644
--- a/cli/options/src/lib.rs
+++ b/cli/options/src/lib.rs
@@ -275,7 +275,8 @@ pub enum ExporterCommand {
         output_file: PathOrDash,
         /// Whether the bodies are exported as THIR, built MIR, const
         /// MIR, or a combination. Repeat this option to extract a
-        /// combination (e.g. `-k thir -k mir-built`).
+        /// combination (e.g. `-k thir -k mir-built`). Pass `--kind`
+        /// alone with no value to disable body extraction.
         #[arg(
             value_enum,
             short,
diff --git a/engine/bin/lib.ml b/engine/bin/lib.ml
index cae1b1bb3..d45b035cc 100644
--- a/engine/bin/lib.ml
+++ b/engine/bin/lib.ml
@@ -62,7 +62,8 @@ let run (options : Types.engine_options) : Types.output =
       (module M : Backend.T with type BackendOptions.t = options_type)
       (backend_options : options_type) : Types.file list =
     let open M in
-    Concrete_ident.ImplInfoStore.init options.impl_infos;
+    Concrete_ident.ImplInfoStore.init
+      (Concrete_ident_generated.impl_infos @ options.impl_infos);
     let include_clauses =
       options.backend.translation_options.include_namespaces
     in
diff --git a/engine/default.nix b/engine/default.nix
index 3c3c82aaa..a8b9c3be8 100644
--- a/engine/default.nix
+++ b/engine/default.nix
@@ -2,6 +2,7 @@
   ocamlPackages,
   fetchzip,
   hax-rust-frontend,
+  hax-engine-names-extract,
   rustc,
   nodejs,
   jq,
@@ -81,6 +82,7 @@
     nativeBuildInputs = [
       rustc
       hax-rust-frontend
+      hax-engine-names-extract
       nodejs
       ocamlPackages.js_of_ocaml-compiler
       jq
@@ -89,9 +91,11 @@
     passthru = {
       docs = hax-engine.overrideAttrs (old: {
         name = "hax-engine-docs";
-        nativeBuildInputs = old.nativeBuildInputs ++ [
-          ocamlPackages.odoc
-        ];
+        nativeBuildInputs =
+          old.nativeBuildInputs
+          ++ [
+            ocamlPackages.odoc
+          ];
         buildPhase = ''dune build @doc'';
         installPhase = "cp -rf _build/default/_doc/_html $out";
       });
diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml
index 5c8657fc7..fecef6406 100644
--- a/engine/lib/concrete_ident/concrete_ident.ml
+++ b/engine/lib/concrete_ident/concrete_ident.ml
@@ -174,8 +174,8 @@ end = struct
     state :=
       impl_infos
       |> List.map ~f:(map_fst Imported.of_def_id)
-      |> Hashtbl.of_alist_exn (module T)
-      |> Option.some
+      |> Hashtbl.of_alist_multi (module T)
+      |> Hashtbl.map ~f:List.hd_exn |> Option.some
 
   let get_state () =
     match !state with
diff --git a/engine/lib/concrete_ident/generate.sh b/engine/lib/concrete_ident/generate.sh
deleted file mode 100755
index ff84f7569..000000000
--- a/engine/lib/concrete_ident/generate.sh
+++ /dev/null
@@ -1,30 +0,0 @@
-#!/usr/bin/env bash
-
-RUST_SOURCE=$(cat "$1")
-TEMPDIR=$(mktemp -d)
-trap '{ rm -rf -- "$TEMPDIR/"; }' EXIT
-DIR="$TEMPDIR/rust-primitives"
-
-mkdir "$DIR" && cd "$DIR"
-
-cargo init --lib
-
-echo "$RUST_SOURCE" > src/lib.rs
-
-cargo hax json --include-extra -o - | jq -r "$(cat - <<JQ_SCRIPT
-  .def_ids | . as \$ids
-  | map(  (.krate | ((.[0:1] | ascii_upcase) + .[1:]))
-        + "__"
-        + ( .path | map(
-              (.data | if type == "object" then to_entries | first | .value else . end)
-            + (.disambiguator | if . == 0 then "" else "_" + (. | tostring) end)
-            ) | join("__"))) as \$names
-  | "type name = " + (\$names | join(" | \\n"))
-  + "\\nmodule Values = struct\\n"
-  + ( keys
-    | map(. as \$i | "let parsed_" + \$names[\$i] + " = Types.parse_def_id (Yojson.Safe.from_string {hax_gen_def_id|" + (\$ids[\$i] | tojson) + "|hax_gen_def_id})")
-    | join("\\n"))
-  + "end\\nlet def_id_of: name -> Types.def_id = function "
-  + (\$names | map(. + " -> Values.parsed_" + .) | join(" | \\n"))
-JQ_SCRIPT
-)"
diff --git a/engine/lib/dune b/engine/lib/dune
index dc2f1a0a6..42f5ff846 100644
--- a/engine/lib/dune
+++ b/engine/lib/dune
@@ -48,12 +48,12 @@
 (rule
  (target concrete_ident_generated.ml)
  (deps
-  (:generate_sh concrete_ident/generate.sh)
-  (:names concrete_ident/names.rs))
+  (alias universe-hash)
+  (env_var HAX_ENGINE_NAMES_EXTRACT_BINARY))
  (action
   (with-stdout-to
    concrete_ident_generated.ml
-   (run bash %{generate_sh} %{names}))))
+   (run %{env:HAX_ENGINE_NAMES_EXTRACT_BINARY=hax-engine-names-extract}))))
 
 (rule
  (target types.ml)
diff --git a/engine/names/Cargo.toml b/engine/names/Cargo.toml
new file mode 100644
index 000000000..6082c8200
--- /dev/null
+++ b/engine/names/Cargo.toml
@@ -0,0 +1,13 @@
+[package]
+name = "hax-engine-names"
+version.workspace = true
+authors.workspace = true
+license.workspace = true
+homepage.workspace = true
+edition.workspace = true
+repository.workspace = true
+readme.workspace = true
+description = "Dummy crate containing all the Rust names the hax engine should be aware of"
+
+[dependencies]
+
diff --git a/engine/names/README.md b/engine/names/README.md
new file mode 100644
index 000000000..bb696a0aa
--- /dev/null
+++ b/engine/names/README.md
@@ -0,0 +1,52 @@
+# `hax-engine-names`
+
+## Purpose of the crate
+The crate `hax-engine-names` is a dummy crate that contains all the
+Rust names the engine should be aware of.
+
+For instance, the engine needs to know about `Some` and `None` to
+reconstruct loops: Rust desugars `for .. in iterator {..}` loops into
+loops with pattern matching on `iterator.next()`, which returns an
+option.
+
+## How to edit this crate
+If you need a special treatment for a Rust name in the engine, you
+should just add a piece of code that is using it.
+
+For example, to make the name `Some` available to the engine, one
+could add the following function at the end of the `src/lib.rs` file:
+
+```rust
+fn some(x: Option<()>) {
+    match x {
+        Some(_) => (),
+        _ => (),
+    }
+}
+```
+
+Note this will also make `Option` available.
+
+## How names are generated in OCaml
+The subcrate `hax-engine-names-extract` runs `cargo hax into json` on
+the crate `hax-engine-names`, and extracts all the names it finds,
+along with other information.
+
+Those names are compiled into the enumeration type
+`Concrete_ident_generated.name`. You can look at those names by
+running `hax-engine-names-extract | less`. As an example,
+`core::option::Option::None` is made available as the
+`Core__option__Option__None` variant.
+
+## How to match a name in the engine
+The functions `Concrete_ident.eq_name` and `Global_ident.eq_name`
+allow for comparing `Concrete_ident.t` and `Global_ident.t` with
+`Concrete_ident_generated.name`.
+
+For example, the expression `Concrete_ident.eq_name
+Core__option__Option__None my_concrete_ident` checks whether the
+concrete ident `my_concrete_ident` is `core::option::Option::None`.
+
+## How to build a concrete ident out of a name
+See the function `Concrete_ident.of_name`.
+
diff --git a/engine/names/extract/Cargo.toml b/engine/names/extract/Cargo.toml
new file mode 100644
index 000000000..bf8437d5f
--- /dev/null
+++ b/engine/names/extract/Cargo.toml
@@ -0,0 +1,20 @@
+[package]
+name = "hax-engine-names-extract"
+version.workspace = true
+authors.workspace = true
+license.workspace = true
+homepage.workspace = true
+edition.workspace = true
+repository.workspace = true
+readme.workspace = true
+description = "Helper binary generating an OCaml module"
+
+
+[build-dependencies]
+hax-cli-options-engine.workspace = true
+hax-frontend-exporter.workspace = true
+serde.workspace = true
+serde_json.workspace = true
+cargo_metadata.workspace = true
+tempfile.version = "3.9"
+camino = "1.1"
diff --git a/engine/names/extract/build.rs b/engine/names/extract/build.rs
new file mode 100644
index 000000000..e9482ce69
--- /dev/null
+++ b/engine/names/extract/build.rs
@@ -0,0 +1,159 @@
+use hax_frontend_exporter::{DefId, DefPathItem, DisambiguatedDefPathItem};
+use serde_json;
+use serde_json::Value;
+use std::process::{Command, Stdio};
+
+/// Name of the current crate
+const HAX_ENGINE_NAMES_CRATE: &str = "hax_engine_names";
+/// Path `a::b` needs to be compiled to a OCaml variant name, `::` is
+/// replaced with `SEPARATOR`
+const SEPARATOR: &str = "__";
+/// "Key" for OCaml quoted strings
+const ESCAPE_KEY: &str = "hax_escape_ocaml_json";
+
+fn uppercase_first_letter(s: &str) -> String {
+    let mut c = s.chars();
+    match c.next() {
+        None => String::new(),
+        Some(f) => f.to_uppercase().collect::<String>() + c.as_str(),
+    }
+}
+
+fn disambiguator_to_str(disambiguator: u32) -> String {
+    if disambiguator == 0 {
+        "".into()
+    } else {
+        format!("_{disambiguator}")
+    }
+}
+
+fn def_path_item_to_str(path_item: DefPathItem) -> String {
+    match path_item {
+        DefPathItem::TypeNs(s)
+        | DefPathItem::ValueNs(s)
+        | DefPathItem::MacroNs(s)
+        | DefPathItem::LifetimeNs(s) => s,
+        DefPathItem::CrateRoot => "CrateRoot".into(),
+        DefPathItem::Impl => "Impl".into(),
+        DefPathItem::ForeignMod => "ForeignMod".into(),
+        DefPathItem::Use => "Use".into(),
+        DefPathItem::GlobalAsm => "GlobalAsm".into(),
+        DefPathItem::ClosureExpr => "ClosureExpr".into(),
+        DefPathItem::Ctor => "Ctor".into(),
+        DefPathItem::AnonConst => "AnonConst".into(),
+        DefPathItem::ImplTrait => "ImplTrait".into(),
+        DefPathItem::ImplTraitAssocTy => "ImplTraitAssocTy".into(),
+    }
+}
+
+fn disambiguated_def_path_item_to_str(defpath: DisambiguatedDefPathItem) -> String {
+    let data = def_path_item_to_str(defpath.data);
+    let disambiguator = disambiguator_to_str(defpath.disambiguator);
+    format!("{data}{disambiguator}")
+}
+
+fn def_id_to_str(DefId { krate, path, .. }: &mut DefId) -> String {
+    if krate == HAX_ENGINE_NAMES_CRATE {
+        *krate = "rust_primitives".into();
+    };
+    let path = path
+        .clone()
+        .into_iter()
+        .map(disambiguated_def_path_item_to_str)
+        .collect::<Vec<String>>()
+        .join(SEPARATOR);
+    format!("{}{SEPARATOR}{path}", uppercase_first_letter(&krate))
+}
+
+fn reader_to_str(s: String) -> String {
+    let json: Value = match serde_json::from_str(&s) {
+        Ok(v) => v,
+        Err(e) => panic!("error while parsing JSON: {e}\n\nString was: {}", &s),
+    };
+    let def_ids: Vec<DefId> = serde_json::from_value(json["def_ids"].clone()).unwrap();
+    let impl_infos = json["impl_infos"].clone();
+
+    let def_ids = def_ids
+        .into_iter()
+        .map(|mut did| {
+            let krate_name = def_id_to_str(&mut did);
+            (serde_json::to_string(&did).unwrap(), krate_name)
+        })
+        .collect::<Vec<_>>();
+
+    const TAB: &str = "    ";
+    let mut result = String::new();
+    result += &format!(
+        "type name = \n{TAB}  {}\n",
+        def_ids
+            .iter()
+            .map(|(_, def_name)| format!("{def_name}"))
+            .collect::<Vec<_>>()
+            .join(&format!("\n{TAB}| "))
+    );
+
+    result += "\n";
+    result += "module Values = struct\n";
+    for (json, name) in &def_ids {
+        result += &format!("{TAB}let parsed_{name} = Types.parse_def_id (Yojson.Safe.from_string {}{ESCAPE_KEY}|{}|{ESCAPE_KEY}{})\n", "{", json, "}");
+    }
+    result += "end\n\n";
+
+    result += &format!(
+        "let def_id_of: name -> Types.def_id = function\n{TAB}  {}\n\n",
+        def_ids
+            .iter()
+            .map(|(_, n)| format!("{n} -> Values.parsed_{n}"))
+            .collect::<Vec<_>>()
+            .join(&format!("\n{TAB}| "))
+    );
+
+    result += &format!("let impl_infos_json_list = match Yojson.Safe.from_string {}{ESCAPE_KEY}|{}|{ESCAPE_KEY}{} with | `List l -> l | _ -> failwith \"Expected a list of `def_id * impl_infos`\"\n\n", "{", serde_json::to_string(&impl_infos).unwrap(), "}");
+    result +=
+        &format!("let impl_infos = Base.List.map ~f:(function | `List [did; ii] -> (Types.parse_def_id did, Types.parse_impl_infos ii) | _ -> failwith \"Expected tuple\") impl_infos_json_list");
+
+    result
+}
+
+fn target_dir(suffix: &str) -> camino::Utf8PathBuf {
+    let metadata = cargo_metadata::MetadataCommand::new().exec().unwrap();
+    let mut dir = metadata.target_directory;
+    dir.push(suffix);
+    dir
+}
+
+fn get_json() -> String {
+    let mut cmd = Command::new("cargo-hax");
+    cmd.args([
+        "hax",
+        "-C",
+        "-p",
+        "hax-engine-names",
+        "--lib",
+        ";",
+        "json",
+        "--include-extra",
+        "-o",
+        "-",
+    ])
+    .stdout(Stdio::piped())
+    .stderr(Stdio::piped());
+
+    cmd.env("CARGO_TARGET_DIR", target_dir("hax"));
+    for env in ["DYLD_FALLBACK_LIBRARY_PATH", "LD_LIBRARY_PATH"] {
+        cmd.env_remove(env);
+    }
+    let out = cmd.output().unwrap();
+    let stdout = String::from_utf8(out.stdout).unwrap();
+    let stderr = String::from_utf8(out.stderr).unwrap();
+    eprintln!("{}", stderr);
+    stdout
+}
+
+fn main() {
+    std::fs::write(
+        format!("{}/module.ml", std::env::var("OUT_DIR").unwrap()),
+        reader_to_str(get_json()),
+    )
+    .unwrap()
+}
diff --git a/engine/names/extract/src/main.rs b/engine/names/extract/src/main.rs
new file mode 100644
index 000000000..8a6392da9
--- /dev/null
+++ b/engine/names/extract/src/main.rs
@@ -0,0 +1,5 @@
+const OCAML_MODULE: &str = include_str!(concat!(env!("OUT_DIR"), "/module.ml"));
+
+fn main() {
+    println!("{}", OCAML_MODULE);
+}
diff --git a/engine/lib/concrete_ident/names.rs b/engine/names/src/lib.rs
similarity index 100%
rename from engine/lib/concrete_ident/names.rs
rename to engine/names/src/lib.rs
diff --git a/engine/utils/universe-hash.sh b/engine/utils/universe-hash.sh
index 029c1fae9..fbec46d95 100755
--- a/engine/utils/universe-hash.sh
+++ b/engine/utils/universe-hash.sh
@@ -20,19 +20,26 @@ function hash() {
     fi
 }
 
-HAX_JSON_SCHEMA_EXPORTER_BINARY=${HAX_JSON_SCHEMA_EXPORTER_BINARY:-hax-export-json-schemas}
-
-if BIN=$(command -v "$HAX_JSON_SCHEMA_EXPORTER_BINARY"); then
-    hash "$BIN"
-else
+function error() {
     DIAG="looks like it's **NOT** the case!"
     if [[ ":$PATH:" == *":$HOME/.cargo/bin"{,/}":"* ]]; then
         DIAG="this seems to be the case"
     fi
-    echo "Error: could not find [$HAX_JSON_SCHEMA_EXPORTER_BINARY] in PATH." >&2
+    echo "Error: could not find [$1] in PATH." >&2
     echo "Please make sure that:" >&2
-    echo "  - you ran Hax's `setup.sh` script;" >&2
+    echo '  - you ran Hax''s `setup.sh` script;' >&2
     echo "  - you have `~/.cargo/bin` in your PATH ($DIAG)." >&2
     exit 1
-fi
+}
+
+HAX_JSON_SCHEMA_EXPORTER_BINARY=${HAX_JSON_SCHEMA_EXPORTER_BINARY:-hax-export-json-schemas}
+HAX_ENGINE_NAMES_EXTRACT_BINARY=${HAX_ENGINE_NAMES_EXTRACT_BINARY:-hax-engine-names-extract}
+
+for binary in "$HAX_JSON_SCHEMA_EXPORTER_BINARY" "$HAX_ENGINE_NAMES_EXTRACT_BINARY"; do
+    if BIN=$(command -v "$binary"); then
+        hash "$BIN"
+    else
+        error "$binary"
+    fi
+done
 
diff --git a/flake.nix b/flake.nix
index 2111bda9a..9b37e7a10 100644
--- a/flake.nix
+++ b/flake.nix
@@ -47,6 +47,7 @@
           inherit rustc ocamlformat rustfmt fstar;
           hax-engine = pkgs.callPackage ./engine {
             hax-rust-frontend = packages.hax-rust-frontend.unwrapped;
+            hax-engine-names-extract = packages.hax-rust-frontend.hax-engine-names-extract;
             inherit rustc;
           };
           hax-rust-frontend = pkgs.callPackage ./cli {
diff --git a/setup.sh b/setup.sh
index 5aa360a22..73dbcc5c9 100755
--- a/setup.sh
+++ b/setup.sh
@@ -44,7 +44,7 @@ ensure_node_is_recent_enough() {
 
 # Installs the Rust CLI & frontend, providing `cargo-hax` and `driver-hax`
 install_rust_binaries() {
-    for i in driver subcommands; do
+    for i in driver subcommands ../engine/names/extract; do
         (
             set -x
             cargo install --force --path "cli/$i"
diff --git a/test-harness/src/command_hax_ext.rs b/test-harness/src/command_hax_ext.rs
index bba0b9d85..ff404a25f 100644
--- a/test-harness/src/command_hax_ext.rs
+++ b/test-harness/src/command_hax_ext.rs
@@ -43,6 +43,7 @@ impl CommandHaxExt for Command {
                         .args(&["build"])
                         .args(dune_jobs_args())
                         .env("HAX_JSON_SCHEMA_EXPORTER_BINARY", cargo_bin("hax-export-json-schemas"))
+                        .env("HAX_ENGINE_NAMES_EXTRACT_BINARY", cargo_bin("hax-engine-names-extract"))
                         .current_dir(engine_dir.clone())
                         .status()
                         .unwrap()