aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/Make
diff options
context:
space:
mode:
authorMaxime Dénès2017-06-07 11:23:13 +0200
committerGitHub2017-06-07 11:23:13 +0200
commit91a31b33e198ae7e1a492931963d6daef52957e5 (patch)
tree6480095ba152ff892d21dc476dd969aa59cb9e04 /mathcomp/Make
parent661b791747c6d1784160ee289945d336b54239e2 (diff)
parentcd7ba12978ee90c2bf1e59584ebf95e9ed275fb2 (diff)
Merge pull request #129 from maximedenes/ssr-merge
Ssr merge
Diffstat (limited to 'mathcomp/Make')
-rw-r--r--mathcomp/Make2
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/Make b/mathcomp/Make
index a7ffeb0..e259330 100644
--- a/mathcomp/Make
+++ b/mathcomp/Make
@@ -129,6 +129,7 @@ ssreflect/ssrbool.v
ssreflect/ssreflect.v
ssreflect/ssrfun.v
ssreflect/ssrnat.v
+ssreflect/ssrnotations.v
ssreflect/tuple.v
ssrtest/absevarprop.v
ssrtest/binders_of.v
@@ -173,7 +174,6 @@ ssrtest/view_case.v
ssrtest/wlogletin.v
ssrtest/wlog_suff.v
ssrtest/wlong_intro.v
-ssreflect.ml4
-I .
-R . mathcomp