aboutsummaryrefslogtreecommitdiff
path: root/.gitignore
diff options
context:
space:
mode:
authorEnrico Tassi2015-03-09 13:35:08 +0100
committerEnrico Tassi2015-03-09 16:21:23 +0100
commit155e671f7b83293ae327ddbd252d1d1ac961ab9a (patch)
tree7bb826abaa20f3fe5ac57e0348be14e8641b5b75 /.gitignore
parentfc84c27eac260dffd8f2fb1cb56d599f1e3486d9 (diff)
some work on ssreflect and discrete
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore9
1 files changed, 9 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..4632509
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,9 @@
+*.d
+*.vo
+*.cm*
+*~
+*.glob
+*.aux
+*.a
+*.o
+Make*.coq