diff --git a/CoqMakefile.local b/CoqMakefile.local
deleted file mode 100644
index 9ac1e9d..0000000
--- a/CoqMakefile.local
+++ /dev/null
@@ -1,2 +0,0 @@
-clean::
-	$(HIDE)rm -f CoqMakefile CoqMakefile.conf
diff --git a/Makefile b/Makefile
index 4332ff0..55119cb 100644
--- a/Makefile
+++ b/Makefile
@@ -1,19 +1,19 @@
-# KNOWNTARGETS will not be passed along to CoqMakefile
-KNOWNTARGETS := CoqMakefile
+# KNOWNTARGETS will not be passed along to RocqMakefile
+KNOWNTARGETS := RocqMakefile
 # 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
+KNOWNFILES := Makefile _RocqProject
 
-.DEFAULT_GOAL := invoke-coqmakefile
+.DEFAULT_GOAL := invoke-rocqmakefile
 
-CoqMakefile: Makefile _CoqProject
-	$(COQBIN)rocq makefile -f _CoqProject -o CoqMakefile
+RocqMakefile: Makefile _RocqProject
+	$(ROCQBIN)rocq makefile -f _RocqProject -o RocqMakefile
 
-invoke-coqmakefile: CoqMakefile
-	$(MAKE) --no-print-directory -f CoqMakefile $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS))
+invoke-rocqmakefile: RocqMakefile
+	$(MAKE) --no-print-directory -f RocqMakefile $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS))
 
-.PHONY: invoke-coqmakefile $(KNOWNFILES)
+.PHONY: invoke-rocqmakefile $(KNOWNFILES)
 
 # This should be the last rule, to handle any targets not declared above
-%: invoke-coqmakefile
+%: invoke-rocqmakefile
 	@true
diff --git a/_CoqProject b/_RocqProject
similarity index 100%
rename from _CoqProject
rename to _RocqProject