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/tests/test_query_extra_dep.v b/tests/test_query_extra_dep.v new file mode 100644 index 000000000..c10dded36 --- /dev/null +++ b/tests/test_query_extra_dep.v @@ -0,0 +1,7 @@ +From elpi Require Import elpi. + +From unreleased Extra Dependency "elpi_elaborator.elpi" as elab. + +Elpi Query lp:{{ coq.extra-dep "elab" _ }}. + +Fail Elpi Query lp:{{ coq.extra-dep "foo" (some _) }}.