aboutsummaryrefslogtreecommitdiff
path: root/.make/coq.mk
diff options
context:
space:
mode:
Diffstat (limited to '.make/coq.mk')
-rw-r--r--.make/coq.mk28
1 files changed, 0 insertions, 28 deletions
diff --git a/.make/coq.mk b/.make/coq.mk
deleted file mode 100644
index bab225be7..000000000
--- a/.make/coq.mk
+++ /dev/null
@@ -1,28 +0,0 @@
-# © 2012–2015 the Massachusetts Institute of Technology
-# @author bbaren + rsloan
-
-COQC = coqc
-COQDEP = coqdep
-
-COMPILE.v = $(COQC) -q $(COQLIBS)
-
-.PHONY: check_fiat check_bedrock
-
-check_fiat:
- @perl -e \
- 'if(! -d "./fiat") { print("you need to link fiat to ./fiat\n"); exit(1) }'
-
-check_bedrock:
- @perl -e \
- 'if(! -d "./bedrock") { print("you need to link bedrock to ./bedrock\n"); exit(1) }'
-
-%.vo %.glob: %.v.d
- $(COMPILE.v) $*
-
-%.v.d: %.v
- @$(COQDEP) -I . $(COQLIBS) "$<" >"$@" \
- || (RV=$$?; rm -f "$@"; exit $${RV})
-
-define coq-generated
-$1.vo $1.v.d $1.glob
-endef