aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2014-05-22 10:35:52 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2014-05-22 10:35:52 +0200
commitcc63a961f846e6e00f56d4c1e98d80fafbfb17b8 (patch)
tree33f1189e862fcb3a952cc723818f360971013903 /.gitignore
parent9c927ebdd7e72bb4ae39b549f55f375d66683be5 (diff)
Ignore generated file.
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore1
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index 6624f901a..7a8b9e625 100644
--- a/.gitignore
+++ b/.gitignore
@@ -133,6 +133,7 @@ tactics/tauto.ml
tactics/eauto.ml
tactics/hipattern.ml
tactics/class_tactics.ml
+tactics/coretactics.ml
tactics/rewrite.ml
tactics/eqdecide.ml
tactics/extratactics.ml