diff --git a/Changelog.md b/Changelog.md
index 39ce8a438..98d9ecfc4 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -15,6 +15,7 @@ Requires Elpi 1.16.5 and Coq 8.18.
 - Change `coq.ltac.call-ltac1` now accepts either a string (tactic name) or
   a tactic expression (of type `ltac1-tactic`)
 - New `ltac_tactic:(...)` syntax to pass tactic expressions to Elpi tactics
+- New `coq.extra-dep` predicate
 
 ## [1.19.1] - 30/08/2023
 
diff --git a/_CoqProject.test b/_CoqProject.test
index c6fa00829..ccbfd241e 100644
--- a/_CoqProject.test
+++ b/_CoqProject.test
@@ -52,3 +52,4 @@ tests/test_link_order_import0.v
 tests/test_link_order_import1.v
 tests/test_link_order_import2.v
 tests/test_link_order_import3.v
+tests/test_query_extra_dep.v
diff --git a/coq-builtin.elpi b/coq-builtin.elpi
index fa4f798d4..f0fd40a23 100644
--- a/coq-builtin.elpi
+++ b/coq-builtin.elpi
@@ -1666,6 +1666,12 @@ external pred coq.term->string i:term, o:string.
 % - @holes! (default: false, prints evars as _)
 external pred coq.term->pp i:term, o:coq.pp.
 
+% -- Extra Dependencies -----------------------------------------------
+
+% [coq.extra-dep Identifier FileName] Resolve the file name of an extra
+% dependency. See also Coq's From xxx Extra Dependency yyy as zzz.
+external pred coq.extra-dep i:id, o:option id.
+
 % -- Access to Elpi's data --------------------------------------------
 
 % clauses
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index ebb75198c..28a45a10b 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -3884,6 +3884,17 @@ Supported attributes:
      state, !: s, [])),
   DocAbove);
 
+  LPDoc "-- Extra Dependencies -----------------------------------------------";
+
+  MLCode(Pred("coq.extra-dep",
+    In(id, "Identifier",
+    Out(option id, "FileName",
+    Easy "Resolve the file name of an extra dependency. See also Coq's From xxx Extra Dependency yyy as zzz.")),
+  (fun id _ ~depth ->
+    !: (try Some (ComExtraDeps.query_extra_dep (Names.Id.of_string id))
+        with Not_found -> None))),
+  DocAbove);
+
   LPDoc "-- Access to Elpi's data --------------------------------------------";
 
    (* Self modification *)
diff --git a/tests/test_query_extra_dep.v b/tests/test_query_extra_dep.v
new file mode 100644
index 000000000..32020f17c
--- /dev/null
+++ b/tests/test_query_extra_dep.v
@@ -0,0 +1,9 @@
+From elpi Require Import elpi.
+
+From unreleased Extra Dependency "elpi_elaborator.elpi" as elab.
+
+Elpi Command test.
+
+Elpi Query lp:{{ coq.extra-dep "elab" (some P) }}.
+
+Elpi Query lp:{{ coq.extra-dep "foo" none }}.