diff --git a/.gitignore b/.gitignore
index 7e0b32f501140ca3c07ffb9c24264d84aba2ed11..9df41c19b7cdef75dcc0fade4ac608bcaf12761a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,5 +1,7 @@
 *.vo
 *.vio
+*.vos
+*.vok
 *.v.d
 .coqdeps.d
 *.glob