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

Remove compatibility with Coq.8.4

4 files changed, 8 insertions, 83 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