aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/discrete/Make
diff options
context:
space:
mode:
authorEnrico Tassi2015-03-09 13:35:08 +0100
committerEnrico Tassi2015-03-09 16:21:23 +0100
commit155e671f7b83293ae327ddbd252d1d1ac961ab9a (patch)
tree7bb826abaa20f3fe5ac57e0348be14e8641b5b75 /mathcomp/discrete/Make
parentfc84c27eac260dffd8f2fb1cb56d599f1e3486d9 (diff)
some work on ssreflect and discrete
Diffstat (limited to 'mathcomp/discrete/Make')
-rw-r--r--mathcomp/discrete/Make15
1 files changed, 15 insertions, 0 deletions
diff --git a/mathcomp/discrete/Make b/mathcomp/discrete/Make
new file mode 100644
index 0000000..bfbbfe2
--- /dev/null
+++ b/mathcomp/discrete/Make
@@ -0,0 +1,15 @@
+all.v
+bigop.v
+binomial.v
+choice.v
+div.v
+finfun.v
+fingraph.v
+finset.v
+fintype.v
+generic_quotient.v
+path.v
+prime.v
+tuple.v
+
+-R . mathcomp.discrete