diff options
-rw-r--r-- | .gitignore | 4 |
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 |