aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore6
1 files changed, 0 insertions, 6 deletions
diff --git a/.gitignore b/.gitignore
index d2e2bcb5c..8c14100cd 100644
--- a/.gitignore
+++ b/.gitignore
@@ -104,11 +104,6 @@ tools/coqdep_lexer.ml
tools/coqdoc/cpretty.ml
lib/xml_lexer.ml
-# .mly files
-
-ide/config_parser.ml
-ide/config_parser.mli
-
# .ml4 files
g_*.ml
@@ -147,7 +142,6 @@ ide/coqide_main_opt.ml
# other auto-generated files
-ide/undo.mli
toplevel/mltop.optml
toplevel/mltop.byteml
kernel/byterun/coq_jumptbl.h