Suppression traducteur

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7846 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 0 insertions, 123 deletions

diff --git a/tools/check-v8 b/tools/check-v8
deleted file mode 100755
index 9dfa0be35..000000000
--- a/tools/check-v8
+++ /dev/null
@@ -1,24 +0,0 @@
-#!/bin/sh
-
-echo ------------------ Producing v8 files -------------------------
-if [ -e v8 ]; then rm -r v8; fi
-if [ -e /tmp/v8.$$ ]; then rm -r /tmp/v8.$$; fi
-cp -pr . /tmp/v8.$$
-mv /tmp/v8.$$ v8
-cd v8
-rm description
-make clean
-make COQFLAGS='-translate -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \
- { echo ---- Failed to translate; exit 1; }
-echo ------------------ Upgrading v8 files -------------------------
-v8files=`find . -name \*.v8`
-for i in $v8files; do
-  j=`dirname $i`/`basename $i .v8`.v
-  echo Upgrading $i
-  mv -u -f $i $j
-done
-echo ------------------ Recompiling v8 files -----------------------
-make clean
-make || { echo ---- Failed to recompile; exit 1; }
-make clean # to save disk space
-echo ------------------ Translation completed ----------------------
diff --git a/tools/restore-v7 b/tools/restore-v7
deleted file mode 100755
index ab8845879..000000000
--- a/tools/restore-v7
+++ /dev/null
@@ -1,9 +0,0 @@
-#!/bin/sh
-
-echo Restoring v7 files from directory v7
-v7files=`find v7 -name \*.v`
-for i in $v7files; do
-  j=`echo $i | sed -e "s@^v7/@@"`
-  echo Restoring $i from v7
-  cp -f $i $j
-done
diff --git a/tools/translate-v8 b/tools/translate-v8
deleted file mode 100755
index 7d71bea99..000000000
--- a/tools/translate-v8
+++ /dev/null
@@ -1,41 +0,0 @@
-#!/bin/sh
-
-if [ -e v7 ]; then
-  echo "Warning: v7 directory found, the files are maybe already translated";
-  sleep 5;
-fi
-echo --------- Producing v8 files in the translation directory -------------
-if [ -e v8 ]; then rm -r v8; fi
-if [ -e /tmp/v7.$$ ]; then rm -r /tmp/v7.$$; fi
-cp -pr . /tmp/v7.$$
-cp -pr /tmp/v7.$$ v8
-cd v8
-rm description toto
-make clean
-make COQFLAGS='-translate -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \
- { echo ---- Failed to translate; exit 1; }
-echo --------- Upgrading files in the translation directory ----------------
-v8files=`find . -name \*.v8`
-for i in $v8files; do
-  j=`dirname $i`/`basename $i .v8`.v
-  echo Upgrading $j in the translation directory
-  mv -u -f $i $j
-done
-echo --------- Recompiling v8 files in the translation directory -----------
-make clean
-make || { echo ---- Failed to recompile; exit 1; }
-echo --------- Saving v7 files in directory v7 -----------------------------
-/bin/rm -r ../v7
-mv /tmp/v7.$$ ../v7
-echo Saving v7 files done
-echo --------- Upgrading files in current directory ------------------------
-vfiles=`find . -name \*.v`
-cd ..
-for i in $vfiles; do
-  echo Upgrading $i in current directory
-  mv -u -f v8/$i $i
-done
-echo --------- Translation completed ---------------------------------------
-echo Old files are in directory '"v7"'
-echo New files are in current directory
-echo You can now remove the translation directory '"v8"'
diff --git a/tools/translate_V6-3-1_to_V7-0 b/tools/translate_V6-3-1_to_V7-0
deleted file mode 100755
index 10e7f1403..000000000
--- a/tools/translate_V6-3-1_to_V7-0
+++ /dev/null
@@ -1,27 +0,0 @@
-#! /bin/sh
-
-echo "This shell script performs the following transformations:"
-echo "- Insertion of a space after a dot not followed by a separator"
-echo "- Insertion of a space between consecutive ~ and < and between"
-echo "  consecutive | and < assumed to be part of distinct tokens"
-echo "- Various renamings of commands as described in document Changes.ps"
-
-for i in $*
-  do sed -e "s/\.\([A-Z]\)/\. \1/g" -e "s/AddPath/Add LoadPath/g" \
-    -e "s/~</~ </g" -e "s/|</| </g" \
-    -e "s/AddPath/Add LoadPath/g" -e "s/DelPath/Remove LoadPath/g" \
-    -e "s/AddRecPath/Add Rec LoadPath/g" \
-    -e "s/Implicit  *Arguments  *On/Set Implicit Arguments/g" \
-    -e "s/Implicit *Arguments *Off/Unset Implicit Arguments/g" \
-    -e "s/Begin *Silent/Set Silent/g" -e "s/End *Silent/Unset Silent/g" \
-    -e "s/Print *Path/Print Coercion Paths/g" \
-    $i > $i.tmp$$
-  if diff $i.tmp$$ $i > /dev/null
-    then
-      rm $i.tmp$$
-    else
-      echo Le fichier $i a été modifié
-      mv $i.tmp$$ $i
-  fi
-  done
-echo
diff --git a/tools/upgrade-v8 b/tools/upgrade-v8
deleted file mode 100755
index 36d0bf8c2..000000000
--- a/tools/upgrade-v8
+++ /dev/null
@@ -1,22 +0,0 @@
-#!/bin/sh
-
-mv v7 v7.bak
-
-echo ---------------- Saving v7 files into directory v7 ------------------
-vfiles=`find . -name \*.v`
-for i in $vfiles; do
-  if expr $i : 'v7\.bak/.*\.v' > /dev/null ; then continue ; fi
-  if expr $i : 'v7/.*\.v' > /dev/null ; then continue ; fi
-  echo Saving $i into v7/$i
-  j=v7/$i
-  mkdir -p `dirname $j`
-  mv -u -f $i $j
-done
-
-echo ---------------- Upgrading files with v8 syntax ---------------------
-v8files=`find . -name \*.v8`
-for i in $v8files; do
-  j=`dirname $i`/`basename $i .v8`.v
-  echo Upgrading $i
-  mv -u -f $i $j
-done