Merge pull request #531 from FissoreD/master-tc-30-10

Master TC 3

.vscode/settings.json

@@ -27,6 +27,7 @@
         "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": [

_CoqProject

@@ -8,27 +8,38 @@
 -Q tests    elpi.tests
 -Q elpi     elpi
 
+# Derive
 -R apps/derive/theories elpi.apps
 -R apps/derive/tests    elpi.apps.derive.tests
 -R apps/derive/examples elpi.apps.derive.examples
+
+# NES
 -R apps/NES/theories elpi.apps
 -R apps/NES/tests    elpi.apps.NES.tests
 -R apps/NES/examples elpi.apps.NES.examples
+
+# Eltac
 -R apps/eltac/theories elpi.apps.eltac
 -R apps/eltac/tests    elpi.apps.eltac.tests
 -R apps/eltac/examples elpi.apps.eltac.examples
--R apps/coercion/theories elpi.apps.coercion
+
+# Coercion
 -R apps/coercion/theories       elpi.apps.coercion
 -R apps/coercion/tests          elpi.apps.tc.coercion
--R apps/coercion/elpi           elpi.apps.coercion
+-I apps/coercion/src
+
+# Type classes
 -R apps/tc/theories       elpi.apps.tc
 -R apps/tc/tests          elpi.apps.tc.tests
 -R apps/tc/elpi           elpi.apps.tc
+-I apps/tc/src
 
+# Coq-elpi 
 theories/elpi.v
 theories/wip/memoization.v
 
 -I src
+
 src/META.coq-elpi
 
 src/coq_elpi_vernacular_syntax.mlg

apps/tc/Makefile.coq.local

@@ -1,19 +1,3 @@
 CAMLPKGS+= -package coq-elpi.elpi
 OCAMLPATH:=../../src/:$(OCAMLPATH)
-export OCAMLPATH
-
-# detection of elpi
-ifeq "$(ELPIDIR)" ""
-ELPIDIR=$(shell ocamlfind query elpi 2>/dev/null)
-endif
-ifeq "$(ELPIDIR)" ""
-$(error Elpi not found, make sure it is installed in your PATH or set ELPIDIR)
-endif
-export ELPIDIR
-
-merlin-hook::
-	echo "S $(abspath $(ELPIDIR))" >> .merlin
-	echo "B $(abspath $(ELPIDIR))" >> .merlin
-	if [ "$(ELPIDIR)" != "elpi/findlib/elpi" ]; then\
-		echo "PKG elpi" >> .merlin;\
-	fi
+export OCAMLPATH