aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore4
1 files changed, 0 insertions, 4 deletions
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