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

2 files changed, 0 insertions, 56 deletions

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