Implement basic tests for "coq.env.query-extra-dep"

LPCIC · Oct 21, 2023 · 4fe9ddc · 4fe9ddc
1 parent ace0641
commit 4fe9ddc
Showing 1 changed file with 7 additions and 0 deletions.
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.env.query-extra-dep "elab" File }}.
+
+Fail Elpi Query lp:{{ coq.env.query-extra-dep "foo" File }}.