aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore4
1 files changed, 2 insertions, 2 deletions
diff --git a/.gitignore b/.gitignore
index 116f88dd7..0193c9dfa 100644
--- a/.gitignore
+++ b/.gitignore
@@ -44,7 +44,6 @@ TAGS
.pc
bin/
_build
-plugins/*/*_mod.ml
myocamlbuild_config.ml
config/Makefile
config/coq_config.ml
@@ -114,7 +113,7 @@ tools/ocamllibdep.ml
tools/coqdoc/cpretty.ml
ide/xml_lexer.ml
-# .ml4 files
+# .ml4 / .mlp files
g_*.ml
@@ -128,6 +127,7 @@ parsing/cLexer.ml
ltac/coretactics.ml
ltac/extratactics.ml
ltac/extraargs.ml
+ltac/profile_ltac_tactics.ml
ide/coqide_main.ml
# other auto-generated files