aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/Make
diff options
context:
space:
mode:
authorErik Martin-Dorel2018-02-25 23:56:29 +0100
committerErik Martin-Dorel2018-02-26 15:23:18 +0100
commitf24095cfbe19c9ddb5ff3dee17a50f715a98acf5 (patch)
tree44c34baf4012a9eeda9ad68476ce72ec7cf00ce8 /mathcomp/Make
parent13f26ccc09f87b222f9601892f085276a6ddb8c0 (diff)
Add ssrmatching.v transitional file
The content of this file is similar to that of ssrfun.v and aims to increase compatibility with Coq 8.6+ for third-party libraries that depend on both math-comp and ssrmatching.v Close #63
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