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