+.PHONY: install uninstall clean test
+
+INTESTS := $(wildcard tests/*.cic)
+OUTTESTS := $(patsubst %, %.test, $(INTESTS))
+gentest: $(OUTTESTS)
+cleantest:
+ rm -f $(OUTTESTS)
+tests/%.cic.test: tests/%.cic regtest
+ time ./regtest -gen $<
+test: regtest
+ ./regtest $(INTESTS) 2> /dev/null
+test.opt: regtest.opt
+ ./regtest.opt $(INTESTS) 2> /dev/null
+envtest: regtest
+ ./regtest -dump $(INTESTS) 2> /dev/null
+envtest.opt: regtest.opt
+ ./regtest.opt -dump $(INTESTS) 2> /dev/null
+librarytest: testlibrary
+ ./testlibrary -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG &
+librarytest.opt: testlibrary.opt
+ ./testlibrary.opt -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG &
+
+MAIN = ./gTopLevel
+ARGS =
+debug:
+ $(OCAMLFIND) query -recursive -predicates byte -a-format \
+ helm-cic_unification | \
+ sed 's/\(.*\)/load_printer "\1"/' \
+ > .debug_script
+ echo "install_printer CicMetaSubst.fppsubst" >> .debug_script
+ echo "install_printer CicMetaSubst.fppterm" >> .debug_script
+ echo "install_printer CicMetaSubst.fppmetasenv" >> .debug_script
+ ledit $(OCAMLDEBUG) \
+ -source .debug_script \
+ $(shell $(OCAMLFIND) query -recursive -i-format $(REQUIRES)) \
+ $(MAIN) $(ARGS)
+
+ifneq ($(MAKECMDGOALS), depend)
+ include .depend
+endif