diff --git a/.gitignore b/.gitignore
index 4b9c49399d8139bf1836735005ea66cbeb31c4db..4ec65516f499b26d3035974999d37110fd2b3cea 100644
--- a/.gitignore
+++ b/.gitignore
@@ -5,7 +5,6 @@
 /html
 *.aux
 Makefile*
-_CoqProject
 *.crashcoqide
 *.v#
 *.cache
diff --git a/_CoqProject b/_CoqProject
new file mode 100644
index 0000000000000000000000000000000000000000..8cc374e6378b9483dd410ba98154e7f0c4038b49
--- /dev/null
+++ b/_CoqProject
@@ -0,0 +1 @@
+-R . rt -arg "-w -notation-overriden,-parsing"
diff --git a/create_makefile.sh b/create_makefile.sh
index 46c35de0c3928a9c2ea46ddce02dc52c42e49eb2..876be759a28af8b348a97a0489eea84067fa7e19 100755
--- a/create_makefile.sh
+++ b/create_makefile.sh
@@ -14,10 +14,6 @@ do
     shift
 done
 
-# Include rt-proofs library in _CoqProject.
-# (For Coq versions >= 8.6, remove spurious warnings.)
-echo -R . rt -arg \"-w -notation-overriden,-parsing\" > _CoqProject
-
 # Compile all *.v files
 if [ "yes" == "$SKIP_CLASSIC" ]
 then