From fb9d9ed9995c6e411f1223d5b53f7b8b6880573e Mon Sep 17 00:00:00 2001
From: Dan Rostovtsev <dan@rostovtsev.org>
Date: Sun, 29 Mar 2026 15:32:40 -0400
Subject: Simple build and README.

---
 Makefile | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 Makefile

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..520ce64
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,29 @@
+# Makefile taken from Rocq Reference Manual 9.0.0
+
+# KNOWNTARGETS will not be passed along to CoqMakefile
+
+KNOWNTARGETS := CoqMakefile extra-stuff extra-stuff2
+
+# KNOWNFILES will not get implicit targets from the final rule, and so
+# depending on them won't invoke the submake
+# Warning: These files get declared as PHONY, so any targets depending
+# on them always get rebuilt
+
+KNOWNFILES := Makefile _CoqProject
+.DEFAULT_GOAL := invoke-coqmakefile
+
+CoqMakefile: Makefile _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o CoqMakefile
+
+invoke-coqmakefile: CoqMakefile
+	$(MAKE) --no-print-directory -f CoqMakefile \
+		$(filter-out $(KNOWNTARGETS), $(MAKECMDGOALS))
+.PHONY: invoke-coqmakefile $(KNOWNFILES)
+
+####################################################################
+##                      Your targets here                         ##
+####################################################################
+
+# This should be the last rule, to handle any targets not declared above
+%: invoke-coqmakefile
+	@true
-- 
cgit v1.3