aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/Make
diff options
context:
space:
mode:
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