diff --git a/src/doc.rs b/src/doc.rs
index 173bd7c..09ce839 100644
--- a/src/doc.rs
+++ b/src/doc.rs
@@ -62,21 +62,32 @@ fn generate_single_target_doc(
     cmd.env("VERUSDOC", verus_doc_value);
     cmd.env("RUSTC_BOOTSTRAP", "1");
 
+    // Add extern dependencies for verus_builtin
+    let builtin_path = verus_target_dir.join("libverus_builtin.rlib");
+    cmd.arg("--extern")
+        .arg(format!("verus_builtin={}", builtin_path.display()));
+
+    // Add extern dependencies for verus_builtin_macros
+    let builtin_macros_path =
+        verus_target_dir.join(format!("verus_builtin_macros{}", verus::DYN_LIB));
+    cmd.arg("--extern").arg(format!(
+        "verus_builtin_macros={}",
+        builtin_macros_path.display()
+    ));
+
+    // Add extern dependencies for verus_state_machine_macros
+    let state_machine_macros_path =
+        verus_target_dir.join(format!("verus_state_machine_macros{}", verus::DYN_LIB));
+    cmd.arg("--extern").arg(format!(
+        "verus_state_machine_macros={}",
+        state_machine_macros_path.display()
+    ));
+
     // Add extern dependencies for vstd
     let vstd_path = verus_target_dir.join("libvstd.rlib");
     cmd.arg("--extern")
         .arg(format!("vstd={}", vstd_path.display()));
 
-    // Add state_machines_macros dependency (proc-macro)
-    let state_machines_macros_path =
-        verus_target_dir.join(format!("verus_state_machines_macros{}", verus::DYN_LIB));
-    if state_machines_macros_path.exists() {
-        cmd.arg("--extern").arg(format!(
-            "verus_state_machines_macros={}",
-            state_machines_macros_path.display()
-        ));
-    }
-
     // Add dependencies that this target actually needs
     let deps = verus::get_local_dependency(target);
     for (_name, dep_target) in deps.iter() {