aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/Makefile
diff options
context:
space:
mode:
authorEnrico Tassi2018-04-20 09:54:12 +0200
committerEnrico Tassi2018-04-20 10:35:01 +0200
commit9352fc35ebe04b8b4e9002f3cf39ee1acbab8cd2 (patch)
treef631c368fbbbe05aa625aa66ed39ac652a2d76a8 /mathcomp/Makefile
parent09bebb67443c0512e01d2c32f4207e09e93f4956 (diff)
remove v8.4 code from Makefile
Diffstat (limited to 'mathcomp/Makefile')
-rw-r--r--mathcomp/Makefile4
1 files changed, 0 insertions, 4 deletions
diff --git a/mathcomp/Makefile b/mathcomp/Makefile
index f6e06b4..e45d627 100644
--- a/mathcomp/Makefile
+++ b/mathcomp/Makefile
@@ -9,11 +9,7 @@ include ssreflect/Makefile.detect-coq-version
# this defined coqmakefile
include ssreflect/Makefile.coq-makefile
-ifeq "$V" "v8.4"
-COQDEP=../etc/utils/ssrcoqdep
-else
COQDEP=$(COQBIN)coqdep
-endif
OLD_MAKEFLAGS:=$(MAKEFLAGS)
MAKEFLAGS+=-B