diff --git a/Cargo.lock b/Cargo.lock
index e1d8e2dee..7c619ec4b 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -525,6 +525,7 @@ dependencies = [
  "cargo_metadata",
  "hax-cli-options-engine",
  "hax-engine-names",
+ "hax-frontend-exporter",
  "serde",
  "serde_json",
  "tempfile",
diff --git a/engine/names/extract/Cargo.toml b/engine/names/extract/Cargo.toml
index 3c845ec32..9604ee100 100644
--- a/engine/names/extract/Cargo.toml
+++ b/engine/names/extract/Cargo.toml
@@ -12,6 +12,7 @@ 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
diff --git a/engine/names/extract/build.rs b/engine/names/extract/build.rs
index 80d22a7e1..2e4a38511 100644
--- a/engine/names/extract/build.rs
+++ b/engine/names/extract/build.rs
@@ -2,14 +2,7 @@ use serde_json;
 use serde_json::Value;
 use std::process::{Command, Stdio};
 
-/// Instead of depending on `hax_frontend_exporter` (that links to
-/// rustc and exposes a huge number of type definitions and their
-/// impls), we just inline a small module here that contains the three
-/// type definition we need. See the module for complementary
-/// informations.
-#[path = "../../../frontend/exporter/src/types/def_id.rs"]
-mod hax_frontend_exporter_def_id;
-use hax_frontend_exporter_def_id::*;
+use hax_frontend_exporter::{DefId, DefPathItem, DisambiguatedDefPathItem};
 
 /// Name of the current crate
 const HAX_ENGINE_NAMES_CRATE: &str = "hax_engine_names";
diff --git a/frontend/exporter/src/types/def_id.rs b/frontend/exporter/src/types/def_id.rs
index 38ab11f7f..2704cf4c5 100644
--- a/frontend/exporter/src/types/def_id.rs
+++ b/frontend/exporter/src/types/def_id.rs
@@ -1,28 +1,15 @@
-//! This module contains the type definition for `DefId` and the types
-//! `DefId` depends on.
-//!
-//! This is purposely a very small isolated module:
-//! `hax-engine-names-extract` uses those types, but we don't want
-//! `hax-engine-names-extract` to have a build dependency on the whole
-//! frontend, that double the build times for the Rust part of hax.
-//!
-//! The feature `extract_names_mode` exists only in the crate
-//! `hax-engine-names-extract`, and is used to turn off the derive
-//! attributes `AdtInto` and `JsonSchema`.
-
-pub use serde::{Deserialize, Serialize};
-
-#[cfg(not(feature = "extract_names_mode"))]
 use crate::{AdtInto, JsonSchema};
+pub use serde::{Deserialize, Serialize};
 
 #[cfg(feature = "full")]
 use crate::{BaseState, SInto};
 
 pub type Symbol = String;
 
-#[derive(Clone, Debug, Serialize, Deserialize, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[cfg_attr(not(feature = "extract_names_mode"), derive(AdtInto, JsonSchema))]
-#[cfg_attr(not(feature = "extract_names_mode"), args(<'a, S: BaseState<'a>>, from: rustc_hir::definitions::DisambiguatedDefPathData, state: S as s))]
+#[derive(
+    Clone, Debug, Serialize, Deserialize, Hash, PartialEq, Eq, PartialOrd, Ord, AdtInto, JsonSchema,
+)]
+#[args(<'a, S: BaseState<'a>>, from: rustc_hir::definitions::DisambiguatedDefPathData, state: S as s)]
 /// Reflects [`rustc_hir::definitions::DisambiguatedDefPathData`]
 pub struct DisambiguatedDefPathItem {
     pub data: DefPathItem,
@@ -30,8 +17,7 @@ pub struct DisambiguatedDefPathItem {
 }
 
 /// Reflects [`rustc_hir::def_id::DefId`]
-#[derive(Clone, Debug, Serialize, Deserialize, PartialEq, Eq, PartialOrd, Ord)]
-#[cfg_attr(not(feature = "extract_names_mode"), derive(JsonSchema))]
+#[derive(Clone, Debug, Serialize, Deserialize, PartialEq, Eq, PartialOrd, Ord, JsonSchema)]
 pub struct DefId {
     pub krate: String,
     pub path: Vec<DisambiguatedDefPathItem>,
@@ -47,9 +33,10 @@ pub struct DefId {
 }
 
 /// Reflects [`rustc_hir::definitions::DefPathData`]
-#[derive(Clone, Debug, Serialize, Deserialize, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[cfg_attr(not(feature = "extract_names_mode"), derive(AdtInto, JsonSchema))]
-#[cfg_attr(not(feature = "extract_names_mode"), args(<'ctx, S: BaseState<'ctx>>, from: rustc_hir::definitions::DefPathData, state: S as state))]
+#[derive(
+    Clone, Debug, AdtInto, JsonSchema, Serialize, Deserialize, Hash, PartialEq, Eq, PartialOrd, Ord,
+)]
+#[args(<'ctx, S: BaseState<'ctx>>, from: rustc_hir::definitions::DefPathData, state: S as state)]
 pub enum DefPathItem {
     CrateRoot,
     Impl,