aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/Make
diff options
context:
space:
mode:
authorMaxime Dénès2017-05-03 09:32:34 +0200
committerMaxime Dénès2017-06-07 11:15:26 +0200
commit96a3c59b4586164e8aa80f53f0f9031fd1167ce8 (patch)
tree8d90a3fd32952657115218b0a3e1eb8464829bcb /mathcomp/Make
parent661b791747c6d1784160ee289945d336b54239e2 (diff)
For trunk, use merged ssr plugin.
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