diff --git a/.gitignore b/.gitignore
index 9c68228a5ec62552a2c95c7416333030a5198e04..4303a4d96e399d67bbac12cdb9230c4070bf22bd 100644
--- a/.gitignore
+++ b/.gitignore
@@ -16,3 +16,4 @@ _opam
 **/case_studies/*/log
 **/case_studies/*/Cargo.lock
 **/rustc-ice-*
+_CoqProject
diff --git a/Makefile b/Makefile
index 2bdf3009361148a253869f0d5a078b09c4d04716..f783c56814d86b2b339ad831ef2b20dae48334f5 100644
--- a/Makefile
+++ b/Makefile
@@ -110,3 +110,26 @@ builddep: builddep/refinedrust-builddep.opam
 	@echo "# Installing package $^."
 	@opam install $(OPAMFLAGS) $^
 .PHONY: builddep
+
+
+### Generating _CoqProject
+define COQPROJECT_BASE_BODY
+# RefinedRust core
+-Q _build/default/theories/lithium lithium
+-Q _build/default/theories/caesium caesium
+-Q _build/default/theories/rust_typing refinedrust
+
+-Q _build/default/case_studies/extra_proofs refinedrust.extra_proofs
+endef
+export COQPROJECT_BASE_BODY
+
+coqproject-base:
+	@echo "$$COQPROJECT_BASE_BODY" > _CoqProject
+
+case_studies/%.coqproject: coqproject-base
+	@echo "-Q _build/default/case_studies/$*/output/$* refinedrust.examples.$*" >> _CoqProject
+
+coqproject-case-studies: $(CASE_STUDIES:=.coqproject)
+
+coqproject: coqproject-base coqproject-case-studies
+
diff --git a/README.md b/README.md
index 7248a06bda74a2e4f5c8c7938269893501e8d436..d9c5bddf95b47ec26894a9585d23aea9570ba5ce 100644
--- a/README.md
+++ b/README.md
@@ -102,7 +102,13 @@ The `lib_load_paths` config option influences where the verifier searches for th
 The crate-level `rr::include` directive can be used to import these proof files (see the description in `SPEC_FORMAT.md`).
 
 ## Proof editing
-In order to interactively look at the generated code using a Coq plugin like Coqtail, VSCoq, or Proof General for the editor of your choice, you need to add a line pointing to the directory of the generated code in the `_CoqProject` file.
+You can interactively look at the generated Coq code using a Coq plugin like Coqtail, VSCoq, Proof General, or CoqIDE for the editor of your choice.
+To do so, your editor needs to know about the Coq project structure.
+As RefinedRust uses the `dune` build system to compile the Coq files, if your editor/plugin supports `dune`, it will automatically find the dependencies.
+
+Otherwise, you will need to explicitly tell it how to find the dependencies in `dune`'s build directory.
+You can generate a basic `_CoqProject` file that is read by your editor using `make coqproject`, which includes RefinedRust's core and the set of case studies.
+If you add a new verification, you can manually add a line for your verification in this file.
 See the existing includes for inspiration.
 
 Changes to the `proof_*.v` files in the generated `proofs` folder are persistent and files are not changed once RefinedRust has generated them once.
diff --git a/_CoqProject b/_CoqProject
deleted file mode 100644
index 10ebca6095e27e83ad6474f8b58a571dbacb6884..0000000000000000000000000000000000000000
--- a/_CoqProject
+++ /dev/null
@@ -1,24 +0,0 @@
--Q _build/default/theories/lithium lithium
--Q _build/default/theories/caesium caesium
--Q _build/default/theories/rust_typing refinedrust
--Q _build/default/case_studies/extra_proofs refinedrust.extra_proofs
-
-# We sometimes want to locally override notation, and there is no good way to do that with scopes.
--arg -w -arg -notation-overridden
-# Cannot use non-canonical projections as it causes massive unification failures
-# (https://github.com/coq/coq/issues/6294).
--arg -w -arg -redundant-canonical-projection
-
-# case studies
--Q _build/default/case_studies/tests/output/tests refinedrust.examples.tests
--Q _build/default/case_studies/paper-examples/output/paper_examples refinedrust.examples.paper_examples
--Q _build/default/case_studies/minivec/output/minivec refinedrust.examples.minivec
--Q _build/default/case_studies/evenint/output/evenint refinedrust.examples.evenint
-
-# stdlib
--Q _build/default/stdlib/vec/target/verify/vec stdlib.alloc.vec
--Q _build/default/stdlib/option/target/verify/option stdlib.option.option
--Q _build/default/stdlib/alloc/target/verify/alloc stdlib.alloc.alloc
--Q _build/default/stdlib/spin/target/verify/spin stdlib.spin.spin
--Q _build/default/stdlib/spin/theories/ stdlib.spin.theories
-