diff --git a/.gitignore b/.gitignore
index e175013..1589c7d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -13,3 +13,4 @@ mutexes.out
 mutexes.pdf
 mutexes.synctex.gz
 comment.cut
+_RocqProject
diff --git a/_CoqProject b/_CoqProject
deleted file mode 100644
index 3a9d7b6..0000000
--- a/_CoqProject
+++ /dev/null
@@ -1,26 +0,0 @@
-# AUTO-GENERATED CONTENT, EDIT `gen-_CoqProject-dune.sh` INSTEAD
-
-# Avoid warnings about entries in this _CoqProject
--arg -w -arg -cannot-open-path
-# Warning settings from `dune` project files
--arg -w -arg -notation-overridden
--arg -w -arg -custom-entry-overridden
--arg -w -arg -redundant-canonical-projection
--arg -w -arg -ambiguous-paths
--arg -w -arg -notation-incompatible-prefix
-# Turn warning on hints into error:
--arg -w -arg +deprecated-hint-without-locality
--arg -w -arg +deprecated-instance-without-locality
--arg -w -arg +deprecated-tacopt-without-locality
--arg -w -arg +future-coercion-class-field
--arg -w -arg +unknown-option
--arg -w -arg +sl-transparent-constants
-
-# Plugin directory.
--I _build/install/default/lib
-
-# Specified logical paths for directories (for .v and .vo files).
--Q _build/default/rocq-brick-libstdcpp/proof/ skylabs.brick.libstdcpp
--Q rocq-brick-libstdcpp/proof/ skylabs.brick.libstdcpp
--Q _build/default/rocq-brick-libstdcpp/test/ skylabs.brick.libstdcpp.test
--Q rocq-brick-libstdcpp/test/ skylabs.brick.libstdcpp.test
diff --git a/rocq-brick-libstdcpp/proof/dune b/rocq-brick-libstdcpp/proof/dune
index c388151..16e0e06 100644
--- a/rocq-brick-libstdcpp/proof/dune
+++ b/rocq-brick-libstdcpp/proof/dune
@@ -4,6 +4,7 @@
 (rocq.theory
  (name skylabs.brick.libstdcpp) ; logical path of this library
  (package rocq-brick-libstdcpp)
+ (generate_project_file)
  (theories
   ; skylabs deps
   Stdlib
diff --git a/rocq-brick-libstdcpp/test/dune b/rocq-brick-libstdcpp/test/dune
index fc9ecc5..c6ace8b 100644
--- a/rocq-brick-libstdcpp/test/dune
+++ b/rocq-brick-libstdcpp/test/dune
@@ -3,6 +3,7 @@
 (include_subdirs qualified)
 (rocq.theory
  (name skylabs.brick.libstdcpp.test) ; logical path of this library
+ (generate_project_file)
  (theories
   ; skylabs.brick.libstdcpp deps
   Stdlib