diff --git a/.forgejo/workflows/test.yml b/.forgejo/workflows/test.yml
index a8868726..7a69a7e5 100644
--- a/.forgejo/workflows/test.yml
+++ b/.forgejo/workflows/test.yml
@@ -17,7 +17,6 @@ jobs:
         with:
           save-if: ${{ github.ref == 'refs/heads/master' }}
       - run: rustup override set 1.93.0
-      - run: make -C rocq-demo
       - run: cargo test
       - run: cargo build --tests --features=unstable-doc
       - run: cargo test --doc --features=unstable-doc
diff --git a/rocq-demo/.gitignore b/rocq-demo/.gitignore
deleted file mode 100644
index 01821130..00000000
--- a/rocq-demo/.gitignore
+++ /dev/null
@@ -1,8 +0,0 @@
-# SPDX-License-Identifier: LGPL-3.0-or-later
-# See Notices.txt for copyright information
-.CoqMakefile.d
-*.aux
-CoqMakefile
-CoqMakefile.conf
-*.glob
-*.vo*
diff --git a/rocq-demo/Makefile b/rocq-demo/Makefile
deleted file mode 100644
index d0d5c9e3..00000000
--- a/rocq-demo/Makefile
+++ /dev/null
@@ -1,31 +0,0 @@
-# SPDX-License-Identifier: LGPL-3.0-or-later
-# See Notices.txt for copyright information
-#
-# Example Makefile wrapper as given on the Rocq documentation
-# https://rocq-prover.org/doc/V9.1.0/refman/practical-tools/utilities.html#building-a-rocq-project-with-rocq-makefile-details
-
-# KNOWNTARGETS will not be passed along to CoqMakefile
-KNOWNTARGETS := CoqMakefile
-# 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-coq-makefile
-
-CoqMakefile: Makefile _CoqProject
-	$(COQBIN)rocq makefile -f _CoqProject -o CoqMakefile
-
-invoke-coq-makefile: CoqMakefile
-	$(MAKE) --no-print-directory -f CoqMakefile $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS))
-
-.PHONY: invoke-coq-makefile $(KNOWNFILES)
-
-####################################################################
-##                      Your targets here                         ##
-####################################################################
-
-# This should be the last rule, to handle any targets not declared above
-%: invoke-coq-makefile
-	@true
diff --git a/rocq-demo/_CoqProject b/rocq-demo/_CoqProject
deleted file mode 100644
index be104207..00000000
--- a/rocq-demo/_CoqProject
+++ /dev/null
@@ -1,5 +0,0 @@
-# SPDX-License-Identifier: LGPL-3.0-or-later
-# See Notices.txt for copyright information
-
--Q . RocqDemo
-.
diff --git a/scripts/check-copyright.sh b/scripts/check-copyright.sh
index 99205bb3..023cd21f 100755
--- a/scripts/check-copyright.sh
+++ b/scripts/check-copyright.sh
@@ -50,7 +50,7 @@ function main()
         /crates/fayalite/tests/ui/*.stderr|/crates/fayalite/tests/sim/expected/*.vcd|/crates/fayalite/tests/sim/expected/*.txt)
             # file that can't contain copyright header
             ;;
-        /.forgejo/workflows/*.yml|*/.gitignore|*.toml|*/Makefile|*/_CoqProject)
+        /.forgejo/workflows/*.yml|*/.gitignore|*.toml)
             check_file "$file" "${POUND_HEADER[@]}"
             ;;
         *.md)