diff --git a/tests/test_query_extra_dep.v b/tests/test_query_extra_dep.v new file mode 100644 index 000000000..cb61ae8c8 --- /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.env.query-extra-dep "elab" File }}. + +Fail Elpi Query lp:{{ coq.env.query-extra-dep "foo" File }}.