aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/Make
diff options
context:
space:
mode:
authorEnrico2018-03-03 10:26:23 +0100
committerGitHub2018-03-03 10:26:23 +0100
commit22692863c2b51cb6b3220e9601d7c237b1830f18 (patch)
tree389049eca835a3ead6c79ca836faf00617e0d91d /mathcomp/Make
parent5811c112c2cf6db25b6a2a1b793d3df5e906b261 (diff)
parentf24095cfbe19c9ddb5ff3dee17a50f715a98acf5 (diff)
Merge pull request #180 from erikmd/export-ssrmatching
Add ssrmatching.v transitional file
Diffstat (limited to 'mathcomp/Make')
-rw-r--r--mathcomp/Make1
1 files changed, 1 insertions, 0 deletions
diff --git a/mathcomp/Make b/mathcomp/Make
index d3c7642..1db29ba 100644
--- a/mathcomp/Make
+++ b/mathcomp/Make
@@ -130,6 +130,7 @@ ssreflect/ssreflect.v
ssreflect/ssrfun.v
ssreflect/ssrnat.v
ssreflect/ssrnotations.v
+ssreflect/ssrmatching.v
ssreflect/tuple.v
ssrtest/absevarprop.v
ssrtest/abstract_var2.v