Implement basic tests for "coq.extra-dep"

LPCIC · Oct 21, 2023 · c8e9e2c · c8e9e2c
1 parent c598a25
commit c8e9e2c
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git 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
@@ -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 _) }}.