diff --git a/.vscode/settings.json b/.vscode/settings.json index c09a25ed7..dc57bf116 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -27,7 +27,6 @@ "src/coq_elpi_vernacular_syntax.ml": true, "**/Makefile.coq": true, "**/Makefile.coq.conf": true, - // "**/.merlin": true }, "restructuredtext.confPath": "${workspaceFolder}/alectryon/recipes/sphinx", "ocaml.server.args": [ diff --git a/_CoqProject b/_CoqProject index 645357b00..37e5a23c2 100644 --- a/_CoqProject +++ b/_CoqProject @@ -18,6 +18,9 @@ -R apps/eltac/tests elpi.apps.eltac.tests -R apps/eltac/examples elpi.apps.eltac.examples -R apps/coercion/theories elpi.apps.coercion +-R apps/coercion/theories elpi.apps.coercion +-R apps/coercion/tests elpi.apps.tc.coercion +-R apps/coercion/elpi elpi.apps.coercion -R apps/tc/theories elpi.apps.tc -R apps/tc/tests elpi.apps.tc.tests -R apps/tc/elpi elpi.apps.tc diff --git a/apps/coercion/theories/coercion.v b/apps/coercion/theories/coercion.v index 2a55adaea..5b8a2742f 100644 --- a/apps/coercion/theories/coercion.v +++ b/apps/coercion/theories/coercion.v @@ -23,7 +23,4 @@ solve (goal Ctx _ Ty Sol [trm V, trm VTy]) _ :- coercion Ctx V VTy Ty Sol. Elpi Accumulate Db coercion.db. Elpi Typecheck. Elpi CoercionFallbackTactic coercion. - -Elpi Query lp:{{ - coq.warning "A" "B" "C" }}. \ No newline at end of file