Updating files + reorganizing everything

2 files changed, 51 insertions, 0 deletions

diff --git a/etc/utils/import_coqfinitgroup.zsh b/etc/utils/import_coqfinitgroup.zsh
new file mode 100755
index 0000000..bf2a0b4
--- /dev/null
+++ b/etc/utils/import_coqfinitgroup.zsh
@@ -0,0 +1,24 @@
+#!/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
new file mode 100755
index 0000000..dd1c068
--- /dev/null
+++ b/etc/utils/ssrcoqdep
@@ -0,0 +1,27 @@
+#!/bin/bash
+
+args="$@"
+echo "calling coqdep on $args" 1>&2
+
+mkdir bkpcoqdep
+
+while [[ $# > 0 ]]
+do
+key="$1"
+
+case $key in
+    *.v)
+        cp $key bkpcoqdep/$key
+	sed "s/^From.*//" -i $key
+    ;;
+    *)
+    ;;
+esac
+shift
+done
+
+COQBIN="$(dirname $(which coqtop))/"
+$COQBIN/coqdep $args
+
+mv bkpcoqdep/* .
+rmdir bkpcoqdep