From e46427d5ed18c4c164f5f0f712fcafa004236a82 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 5 Apr 2020 09:35:12 +0200
Subject: [PATCH] Ignore more.

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

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