-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
-typecheck_uri: typecheck_uri.ml
- $(OCAMLFIND) ocamlc -thread -package helm-cic_proof_checking -linkpkg -o $@ $<
-typecheck_uri.opt: typecheck_uri.ml
- $(OCAMLFIND) opt -thread -package helm-cic_proof_checking -linkpkg -o $@ $<