From cc63a961f846e6e00f56d4c1e98d80fafbfb17b8 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Thu, 22 May 2014 10:35:52 +0200
Subject: Ignore generated file.

---
 .gitignore | 1 +
 1 file changed, 1 insertion(+)

(limited to '.gitignore')

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
-- 
cgit v1.2.3