aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/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/ssreflect/Make
parentfc84c27eac260dffd8f2fb1cb56d599f1e3486d9 (diff)
some work on ssreflect and discrete
Diffstat (limited to 'mathcomp/ssreflect/Make')
-rw-r--r--mathcomp/ssreflect/Make8
1 files changed, 8 insertions, 0 deletions
diff --git a/mathcomp/ssreflect/Make b/mathcomp/ssreflect/Make
index 9e7c5db..6c76897 100644
--- a/mathcomp/ssreflect/Make
+++ b/mathcomp/ssreflect/Make
@@ -6,3 +6,11 @@ ssreflect.v
ssrfun.v
ssrmatching.v
ssrnat.v
+
+ssreflect.mllib
+ssrmatching.mli
+ssrmatching.ml4
+ssreflect.ml4
+
+-I .
+-R . mathcomp.ssreflect