From 40021d41b085276c4c26bc5de7484add920e31f0 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Sat, 18 Jul 2015 14:38:59 +0200
Subject: update to preserve backward compatibility with v8.4

---
 mathcomp/basic/Make     |  2 +-
 mathcomp/basic/Makefile | 22 +++++++++++++++++++++-
 2 files changed, 22 insertions(+), 2 deletions(-)

(limited to 'mathcomp/basic')

diff --git a/mathcomp/basic/Make b/mathcomp/basic/Make
index cd88088..8acef84 100644
--- a/mathcomp/basic/Make
+++ b/mathcomp/basic/Make
@@ -12,4 +12,4 @@ path.v
 prime.v
 tuple.v
 
--R . mathcomp.discrete
+-R . mathcomp.basic
\ No newline at end of file
diff --git a/mathcomp/basic/Makefile b/mathcomp/basic/Makefile
index e872352..8f03823 100644
--- a/mathcomp/basic/Makefile
+++ b/mathcomp/basic/Makefile
@@ -4,6 +4,25 @@ ifeq "$(COQBIN)" ""
 COQBIN=$(dir $(shell which coqtop))/
 endif
 
+BRANCH_coq = $(shell $(COQBIN)/coqtop -v | head -1 | sed 's/.*version \([0-9]\.[0-9]\)[^ ]* .*/v\1/')
+
+HASH_coq = $(shell echo Quit. | $(COQBIN)/coqtop 2>&1 | head -1 | sed 's/^.*(\([a-f0-9]*\)).*/\1/' )
+
+HASH_coq_v85beta1 = eaa3d0b15adf4eb11ffb00ab087746a5b15c4d5d
+
+
+ifeq "$(HASH_coq)" "$(HASH_coq_v85beta1)"
+V=v8.5beta1
+else
+V=$(BRANCH_coq)
+endif
+
+ifeq "$V" "v8.4"
+COQDEP=../../etc/utils/ssrcoqdep
+else
+COQDEP=$(COQBIN)/coqdep
+endif
+
 OLD_MAKEFLAGS:=$(MAKEFLAGS)
 MAKEFLAGS+=-B
 
@@ -12,7 +31,8 @@ MAKEFLAGS+=-B
 %:
 	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
 	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
-		-f Makefile.coq $*
+		-f Makefile.coq $* \
+		COQDEP='$(COQDEP) -c'
 
 .PHONY: clean
 clean:
-- 
cgit v1.2.3