From ea25e8bcf64caac66bcbd33457ee91d56e80fea3 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
Date: Tue, 12 Jul 2016 16:32:12 +0200
Subject: .gitignore: no more generated grammar/*.ml files

---
 .gitignore | 4 ----
 1 file changed, 4 deletions(-)

(limited to '.gitignore')

diff --git a/.gitignore b/.gitignore
index 0d5eee652..8a0c54f8f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -119,10 +119,6 @@ g_*.ml
 
 ide/project_file.ml
 parsing/compat.ml
-grammar/q_util.ml
-grammar/tacextend.ml
-grammar/vernacextend.ml
-grammar/argextend.ml
 parsing/cLexer.ml
 ltac/coretactics.ml
 ltac/extratactics.ml
-- 
cgit v1.2.3