From 979773e99aee5a43693fd1b6256f867255982af1 Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gregory@skylabs-ai.com>
Date: Tue, 19 May 2026 00:26:47 -0400
Subject: [PATCH] Generate _RocqProject

---
 .gitignore                      |  1 +
 _CoqProject                     | 26 --------------------------
 rocq-brick-libstdcpp/proof/dune |  1 +
 rocq-brick-libstdcpp/test/dune  |  1 +
 4 files changed, 3 insertions(+), 26 deletions(-)
 delete mode 100644 _CoqProject

diff --git a/.gitignore b/.gitignore
index e1750138..1589c7dd 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 3a9d7b64..00000000
--- 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 c388151b..16e0e06d 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 fc9ecc5d..c6ace8bb 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