Merge pull request #149 from CohenCyril/no-compat-coq.8.4

Remove compatibility with Coq.8.4

14 files changed, 9 insertions, 226 deletions

diff --git a/etc/ChangeLog b/etc/ChangeLog
index f10e25c..12d6ef4 100644
--- a/etc/ChangeLog
+++ b/etc/ChangeLog
@@ -1,6 +1,10 @@
-07/09/2016 - compatibility with Coq 8.7 and several small fixes - version 1.7
+07/09/2016 - compatibility with Coq 8.7 and several small fixes -
+	version 1.6.2 and upcomming version 1.7
 	* Compatibility with Coq 8.7
+	* Lost compatibility with Coq 8.4
 
+07/09/2016 - compatibility with Coq 8.7 and several small fixes -
+	upcomming version 1.7
 	* New Theorems:
 	   dec_factor_theorem, abstract_context,
 	   mul_bin_down, mul_bin_left
@@ -15,7 +19,8 @@
 	* Plugin:
 	  ssrpattern: compose nicely with Tactic Notation
 
-25/08/2016 - refactoring of algC and complex in ssrnum
+25/08/2016 - refactoring of algC and complex in ssrnum -
+	upcomming version 1.7
 	* ssrnum's interface numClosedFieldType factors some theory from
 	  both complex and algC. Because of that Re, Im, 'i, conjC, n.-root
 	  and sqrtC are not specialized to algC anymore. In case of
diff --git a/etc/INSTALL.md b/etc/INSTALL.md
index b293831..4bc3a95 100644
--- a/etc/INSTALL.md
+++ b/etc/INSTALL.md
@@ -10,7 +10,7 @@ compiling it from sources.
 
 ## REQUIREMENTS
 
-Coq version 8.4pl6 or 8.5 (at the time of writing, beta3)
+Coq version 8.5 to 8.7.0
 
 ## BUILDING
 
@@ -76,27 +76,3 @@ file.
 
 Coq sources have a .v extension. Opening any .v file should
 automatically launch ProofGeneral.
-
-## TRANSITION FROM 1.5 to 1.6
-
-The change of logical/physical paths implied by the reorganization of the
-library causes an incompatibility for users of previous version of the
-Mathematical Components library. For instance the command line
-
-          Require Ssreflect.ssreflect.
-
-does not work anymore.  We propose a replacement schema for such
-command lines that is compatible with both versions 8.4 and 8.5 of
-Coq, namely replacing the previous line with:
-
-          Require Import mathcomp.ssreflect.ssreflect.
-
-          From mathcomp Require Import ssrfun ssrbool ...
-
-The first line loads the ssreflect plugin using its full path.
-Then all other files are loaded from the mathcomp name space.
-The component part (like ssreflect or algebra) is omitted.  All theory files in
-the library follow this schema.
-Note that the From directive has effect only in Coq 8.5. Coq 8.4 ignores it
-and searches for files in all known paths: hence beware of the
-possible name collisions.
diff --git a/etc/utils/import_coqfinitgroup.zsh b/etc/utils/import_coqfinitgroup.zsh
deleted file mode 100755
index bf2a0b4..0000000
--- a/etc/utils/import_coqfinitgroup.zsh
+++ /dev/null
@@ -1,24 +0,0 @@
-#!/bin/zsh
-
-COQFINITGROUP=$1
-
-for f in $COQFINITGROUP/theories/*.v
-  do nf=$(find . -name $(basename $f))
-  echo "copy $f to $nf"
-  cp $f $nf
-done
-for f in $COQFINITGROUP/ssreflect/test/*.v
-  do nf=$(find . -name $(basename $f))
-  echo "copy $f to $nf"
-  cp $f $nf
-done
-sed "s/Require Import ssrmatching\./Require Import mathcomp.ssreflect.ssrmatching./" -i */*.v
-sed "s/Require ssreflect\./Require mathcomp.ssreflect.ssreflect./" -i */*.v
-sed "s/Require Import ssreflect/Require Import mathcomp.ssreflect.ssreflect.\nRequire Import/" -i */*.v
-sed "s/Require Import/From mathcomp Require Import/" -i */*.v
-sed "s/From mathcomp Require Import mathcomp/Require Import mathcomp/" -i */*.v
-sed "s/From mathcomp Require Import BinNat/Require Import BinNat/" -i */*.v
-sed "s/From mathcomp Require Import Arith/Require Import Arith/" -i */*.v
-sed "s/From mathcomp Require Import Bool/Require Import Bool/" -i */*.v
-sed "s/From mathcomp Require Import\.//" -i */*.v
-sed "s/From mathcomp Require Import/From mathcomp\nRequire Import/" -i */*.v
diff --git a/etc/utils/ssrcoqdep b/etc/utils/ssrcoqdep
deleted file mode 100755
index 20e1281..0000000
--- a/etc/utils/ssrcoqdep
+++ /dev/null
@@ -1,32 +0,0 @@
-#!/bin/bash
-
-args="$@"
-echo "calling coqdep on $args" 1>&2
-
-mkdir bkpcoqdep
-
-while [[ $# > 0 ]]
-do
-key="$1"
-
-case $key in
-    *.v)
-	mkdir -p $(dirname bkpcoqdep/$key)
-        cp $key bkpcoqdep/$key
-        sed "s/^From.*//" bkpcoqdep/$key > $key
-    ;;
-    *)
-    ;;
-esac
-shift
-done
-
-COQBIN="$(dirname $(which coqtop))/"
-$COQBIN/coqdep $args
-
-for f in $(find bkpcoqdep -name "*.v")
-do
-mv $f ${f##bkpcoqdep/}
-done
-
-rm -rf bkpcoqdep
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