diff --git a/.gitignore b/.gitignore
index e94a6d3546..35760736a6 100644
--- a/.gitignore
+++ b/.gitignore
@@ -156,7 +156,8 @@ bin
 # generated by dune build -p
 *.install
 
-# Generated by dune
+# Generated by the build system
+theories/_CoqProject
 _RocqProject
 
 .dune-stamp
diff --git a/theories/Makefile b/theories/Makefile
index c6e9b05a5d..05242d8bce 100644
--- a/theories/Makefile
+++ b/theories/Makefile
@@ -4,9 +4,16 @@ ROCQMAKEOPTIONS?=
 ROCQMAKEFILEOPTIONS?=
 
 .PHONY: all install clean
-all install clean: Makefile.coq
+all install: Makefile.coq
 	+$(MAKE) -f $< $(ROCQMAKEOPTIONS) $@
 
+clean: Makefile.coq
+	+$(MAKE) -f $< $(ROCQMAKEOPTIONS) $@
+	rm -f _CoqProject
+
+_CoqProject: gen_CoqProject.sh rocq-flags.conf
+	./$< > $@
+
 Makefile.coq: _CoqProject
 	$(ROCQMAKEFILE) $(ROCQMAKEFILEOPTIONS) -f $< $(shell find . -regex ".*/[^.][^/]*[.]v" -not -name All.v) -o $@
 
diff --git a/theories/_CoqProject b/theories/_CoqProject
deleted file mode 100644
index b34d8dd88a..0000000000
--- a/theories/_CoqProject
+++ /dev/null
@@ -1,9 +0,0 @@
--R . Stdlib
-# When editing below lines, keep the theories/dune file in sync
-# to handle when requiring Rocq >= 9.2
--arg -w -arg -notation-for-abbreviation
--arg -w -arg -ltac2-notation-for-abbreviation
--arg -w -arg -implicit-create-hint-db
--arg -w -arg -implicit-create-rewrite-hint-db
--arg -w -arg -register-all
--arg -w -arg -scheme-rewriting
diff --git a/theories/dune b/theories/dune
index 1238ba603c..d48a7a0ade 100644
--- a/theories/dune
+++ b/theories/dune
@@ -1,11 +1,13 @@
+(rule
+ (action
+  (with-stdout-to rocq-flags
+  (pipe-stdout
+   (cat rocq-flags.conf)
+   (bash "grep '^[^#]\\+' || true")))))
+
 (include_subdirs qualified)
 (rocq.theory
  (name Stdlib)
  (generate_project_file)
+ (flags :standard %{read-lines:rocq-flags})
  (package rocq-stdlib))
-
-(env
- (dev
-  (rocq
-   ;; see theories/_CoqProject for details
-   (flags :standard -w -notation-for-abbreviation -w -ltac2-notation-for-abbreviation -w -implicit-create-hint-db -w -implicit-create-rewrite-hint-db -w -register-all -w -scheme-rewriting))))
diff --git a/theories/gen_CoqProject.sh b/theories/gen_CoqProject.sh
new file mode 100755
index 0000000000..24dbb59ca8
--- /dev/null
+++ b/theories/gen_CoqProject.sh
@@ -0,0 +1,14 @@
+#!/bin/sh
+set -e
+# Script generating the contents of [_CoqProject] from [rocq-flags.conf].
+
+echo "# Generated file, edit [gen_CoqProject.sh] / [rocq-flags.conf] instead."
+
+echo
+echo "# Search path"
+echo "-R . Stdlib"
+
+echo
+echo "# Flags"
+# Adding "-arg " prefix to all non-empty, non-comment lines of [config/flags].
+cat rocq-flags.conf | grep "^[^#]\+" | sed "s/^/-arg /"
diff --git a/theories/rocq-flags.conf b/theories/rocq-flags.conf
new file mode 100644
index 0000000000..6574af2406
--- /dev/null
+++ b/theories/rocq-flags.conf
@@ -0,0 +1,24 @@
+# Specification for custom Rocq compilation flags.
+# Syntax:
+# - One flag per line with no leading/trailing blanks.
+# - Empty lines and lines starting with '#' are ignored.
+
+# Disable some warnings (for Rocq >= 9.2)
+
+-w
+-notation-for-abbreviation
+
+-w
+-ltac2-notation-for-abbreviation
+
+-w
+-implicit-create-hint-db
+
+-w
+-implicit-create-rewrite-hint-db
+
+-w
+-register-all
+
+-w
+-scheme-rewriting