Remove compatibility with Coq.8.4 (and compatibility hacks that went with it)

10 files changed, 1 insertions, 143 deletions

diff --git a/mathcomp/algebra/Makefile b/mathcomp/algebra/Makefile
index ad0cab5..d4e1bca 100644
--- a/mathcomp/algebra/Makefile
+++ b/mathcomp/algebra/Makefile
@@ -4,25 +4,7 @@ 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
 
diff --git a/mathcomp/character/Makefile b/mathcomp/character/Makefile
index ad0cab5..14acb5c 100644
--- a/mathcomp/character/Makefile
+++ b/mathcomp/character/Makefile
@@ -4,24 +4,7 @@ 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
diff --git a/mathcomp/field/Makefile b/mathcomp/field/Makefile
index ad0cab5..14acb5c 100644
--- a/mathcomp/field/Makefile
+++ b/mathcomp/field/Makefile
@@ -4,24 +4,7 @@ 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
diff --git a/mathcomp/fingroup/Makefile b/mathcomp/fingroup/Makefile
index ad0cab5..14acb5c 100644
--- a/mathcomp/fingroup/Makefile
+++ b/mathcomp/fingroup/Makefile
@@ -4,24 +4,7 @@ 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
diff --git a/mathcomp/odd_order/Makefile b/mathcomp/odd_order/Makefile
index ad0cab5..14acb5c 100644
--- a/mathcomp/odd_order/Makefile
+++ b/mathcomp/odd_order/Makefile
@@ -4,24 +4,7 @@ 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
diff --git a/mathcomp/real_closed/Makefile b/mathcomp/real_closed/Makefile
index ad0cab5..14acb5c 100644
--- a/mathcomp/real_closed/Makefile
+++ b/mathcomp/real_closed/Makefile
@@ -4,24 +4,7 @@ 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
diff --git a/mathcomp/solvable/Makefile b/mathcomp/solvable/Makefile
index ad0cab5..14acb5c 100644
--- a/mathcomp/solvable/Makefile
+++ b/mathcomp/solvable/Makefile
@@ -4,24 +4,7 @@ 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
diff --git a/mathcomp/ssreflect/Makefile b/mathcomp/ssreflect/Makefile
index b1dd21e..e4474c2 100644
--- a/mathcomp/ssreflect/Makefile
+++ b/mathcomp/ssreflect/Makefile
@@ -9,11 +9,7 @@ include Makefile.detect-coq-version
 # this defined coqmakefile
 include Makefile.coq-makefile
 
-ifeq "$V" "v8.4"
-COQDEP=../../etc/utils/ssrcoqdep
-else
 COQDEP=$(COQBIN)coqdep
-endif
 
 OLD_MAKEFLAGS:=$(MAKEFLAGS)
 MAKEFLAGS+=-B
@@ -22,7 +18,6 @@ MAKEFLAGS+=-B
 
 %:
 	$(H)[ -e Makefile.coq ] || $(call coqmakefile,.)
-	# Override COQDEP to find only the "right" copy .ml files
 	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
 		-f Makefile.coq $* \
 		COQDEP='$(COQDEP) -exclude-dir plugin -c'
diff --git a/mathcomp/ssreflect/opam b/mathcomp/ssreflect/opam
index 7e1b09c..7e57fa6 100644
--- a/mathcomp/ssreflect/opam
+++ b/mathcomp/ssreflect/opam
@@ -10,7 +10,7 @@ license: "CeCILL-B"
 build: [ make "-j" "%{jobs}%" ]
 install: [ make "install" ]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp'" ]
-depends: [ "coq" { ((>= "8.4pl4" & < "8.8~") | (= "dev"))} ]
+depends: [ "coq" { ((>= "8.5" & < "8.8~") | (= "dev"))} ]
 
 tags: [ "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" ]
 authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ]
diff --git a/mathcomp/ssrtest/Makefile b/mathcomp/ssrtest/Makefile
index ad0cab5..14acb5c 100644
--- a/mathcomp/ssrtest/Makefile
+++ b/mathcomp/ssrtest/Makefile
@@ -4,24 +4,7 @@ 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