wip

LPCIC · Oct 10, 2023 · 1706169 · 1706169
1 parent 8d162d2
commit 1706169
Show file tree

Hide file tree

Showing 8 changed files with 1,502 additions and 3,049 deletions.
diff --git a/Makefile b/Makefile
@@ -21,7 +21,7 @@ export ELPIDIR
 
 DEPS=$(ELPIDIR)/elpi.cmxa $(ELPIDIR)/elpi.cma
 
-APPS=$(addprefix apps/, derive eltac NES locker coercion)
+APPS=$(addprefix apps/, derive eltac NES locker coercion tc)
 
 ifeq "$(COQ_ELPI_ALREADY_INSTALLED)" ""
 DOCDEP=build

diff --git a/apps/coercion/theories/coercion.v b/apps/coercion/theories/coercion.v
@@ -23,4 +23,3 @@ 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.
-}}.
diff --git a/apps/tc/Makefile.coq.local b/apps/tc/Makefile.coq.local
@@ -2,6 +2,15 @@ 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

diff --git a/apps/tc/_CoqProject b/apps/tc/_CoqProject
@@ -7,6 +7,7 @@
 -R elpi       elpi.apps.tc
 
 src/coq_elpi_tc_hook.mlg
+src/coq_elpi_class_tactics_hacked.ml
 src/elpi_tc_plugin.mlpack
 
 -I src/