Apply suggestions from code review

LPCIC · Oct 10, 2023 · 2042eb2 · 2042eb2
1 parent a25b79e
commit 2042eb2
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 4 deletions.
diff --git 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
@@ -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
@@ -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"
 }}.