From d6f19e41b10720092ed607ed8db7940135a90d2d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 26 Mar 2020 00:21:05 +0100
Subject: [PATCH] Ignore more stuff.

---
 .gitignore | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.gitignore b/.gitignore
index 7107983..84be542 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,6 @@
 *.vo
+*.vos
+*.vok
 *.vio
 *.v.d
 .coqdeps.d
-- 
GitLab