From 3365fb1c5fa3d37f23775e7fb3ee4a2a341bb2ef Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 4 May 2018 17:30:44 +0200
Subject: .gitignore fine-tuning

---
 .gitignore | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/.gitignore b/.gitignore
index 73640ea8f7..be4ea26f86 100644
--- a/.gitignore
+++ b/.gitignore
@@ -3,4 +3,7 @@
 Makefile.coq*
 *~
 *.[ao]
-.coqdeps.d
\ No newline at end of file
+.coqdeps.d
+*.vo
+*.glob
+*.aux
-- 
cgit v1.2.3