6 files changed, 19 insertions, 191 deletions
diff --git a/tools/README.emacs b/tools/README.emacs
deleted file mode 100644
index 4d8e3697a0..0000000000
--- a/tools/README.emacs
+++ /dev/null
@@ -1,31 +0,0 @@
-
-DESCRIPTION:
-
-An emacs mode to help editing Coq vernacular files.
-
-AUTHOR:
-
-Jean-Christophe Filliatre (jcfillia@lri.fr),
-	from the Caml mode of Xavier Leroy.
-
-CONTENTS:
-
-    gallina.el     A major mode for editing Coq files in Gnu Emacs
-
-USAGE:
-
-Add the following lines to your .emacs file:
-
-(setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
-(autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t)
-
-The Coq major mode is triggered by visiting a file with extension .v,
-or manually by M-x coq-mode. It gives you the correct syntax table for
-the Coq language, and also a rudimentary indentation facility:
-
-- pressing TAB at the beginning of a line indents the line like the line above
-
-- extra TABs increase the indentation level (by 2 spaces by default)
-
-- M-TAB decreases the indentation level.
-
diff --git a/tools/check-translate b/tools/check-translate
deleted file mode 100755
index acb6f45903..0000000000
--- a/tools/check-translate
+++ /dev/null
@@ -1,23 +0,0 @@
-#!/bin/sh
-
-echo -------------- Producing translated files ---------------------
-rm */*/*.v8 >& /dev/null
-make COQOPTS=-translate theories || { echo ---- Failed to translate; exit 1; }
-if [ -e translated ]; then rm -r translated; fi
-if [ -e successful-translation ]; then rm -r successful-translation; fi
-if [ -e failed-translation ]; then rm -r failed-translation; fi
-mv theories translated
-mkdir theories
-echo -------------------- Upgrading files --------------------------
-cd translated
-for i in */*.v
-do
-  mkdir ../theories/`dirname $i` >& /dev/null
-  mv "$i"8 ../theories/$i
-done
-cd ..
-echo --------------- Recompiling translated files ------------------
-make theories || { echo ---- Failed to recompile; mv theories failed-translation; mv translated theories; exit 1; }
-echo ----------------- Recompilation successful --------------------
-if [ -e successful-translation ]; then rm -r successful-translation; fi
-mv theories successful-translation; mv translated theories
diff --git a/tools/coq-sl.sty b/tools/coq-sl.sty
deleted file mode 100644
index 9f6e5480c9..0000000000
--- a/tools/coq-sl.sty
+++ /dev/null
@@ -1,37 +0,0 @@
-% COQ style option, for use with the coq-latex filter.
-
-\typeout{Document Style option `coq-sl' <7 Apr 92>.}
-
-\ifcase\@ptsize
-    \font\sltt = cmsltt10
-\or \font\sltt = cmsltt10 \@halfmag
-\or \font\sltt = cmsltt10 \@magscale1
-\fi
-
-{\catcode`\^^M=\active %
- \gdef\@coqinputline#1^^M{\tt Coq < #1\par} %
- \gdef\@coqoutputline#1^^M{\sltt#1\par} } %
-\def\@coqblankline{\medskip}
-\chardef\@coqbackslash="5C
-
-\def\coq{
-  \bgroup
-  \flushleft
-  \parindent 0pt
-  \parskip 0pt
-  \let\do\@makeother\dospecials
-  \catcode`\^^M=\active
-  \catcode`\\=0
-  \catcode`\ \active
-  \frenchspacing
-  \@vobeyspaces
-  \let\?\@coqinputline
-  \let\:\@coqoutputline
-  \let\;\@coqblankline
-  \let\\\@coqbackslash
-}
-
-\def\endcoq{
-  \endflushleft
-  \egroup\noindent
-}
diff --git a/tools/coqdoc/dune b/tools/coqdoc/dune
index 8e05c7d97e..b20d9f9b2e 100644
--- a/tools/coqdoc/dune
+++ b/tools/coqdoc/dune
@@ -1,3 +1,9 @@
+(install
+ (section lib)
+ (files
+  (coqdoc.css as tools/coqdoc/coqdoc.css)
+  (coqdoc.sty as tools/coqdoc/coqdoc.sty)))
+
 (executable
  (name main)
  (public_name coqdoc)
diff --git a/tools/dune b/tools/dune
index 05a620fb07..20048fde52 100644
--- a/tools/dune
+++ b/tools/dune
@@ -1,8 +1,11 @@
-(executable
- (name coqc)
- (public_name coqc)
- (modules coqc)
- (libraries coq.toplevel))
+(install
+ (section lib)
+ (files
+  (CoqMakefile.in as tools/CoqMakefile.in)
+  (TimeFileMaker.py as tools/TimeFileMaker.py)
+  (make-one-time-file.py as tools/make-one-time-file.py)
+  (make-both-time-files.py as tools/make-both-time-files.py)
+  (make-both-single-timing-files.py as tools/make-both-single-timing-files.py)))
 
 (executable
  (name coq_makefile)
@@ -10,9 +13,11 @@
  (modules coq_makefile)
  (libraries coq.lib))
 
-(install
- (section lib)
- (files (CoqMakefile.in as tools/CoqMakefile.in)))
+(executable
+ (name coqc)
+ (public_name coqc)
+ (modules coqc)
+ (libraries coq.toplevel))
 
 (executable
  (name coqdep)
diff --git a/tools/mkwinapp.ml b/tools/mkwinapp.ml
deleted file mode 100644
index 226302fb2d..0000000000
--- a/tools/mkwinapp.ml
+++ /dev/null
@@ -1,92 +0,0 @@
-(* OCaml-Win32
- * mkwinapp.ml
- * Copyright (c) 2002-2004 by Harry Chomsky
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Library General Public
- * License as published by the Free Software Foundation; either
- * version 2 of the License, or (at your option) any later version.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
- * Library General Public License for more details.
- *
- * You should have received a copy of the GNU Library General Public
- * License along with this library; if not, write to the Free
- * Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
- *)
-
-(*********************************************************************
- * This program alters an .exe file to make it use the "windows subsystem"
- * instead of the "console subsystem".  In other words, when Windows runs
- * the program, it will not create a console for it.
- *)
-
-(* Pierre Letouzey 23/12/2010 : modification to allow selecting the
-   subsystem to use instead of just setting the windows subsystem *)
-
-(* This tool can be run directly via :
-   ocaml unix.cma mkwinapp.ml [-set|-unset] <filename>
-*)
-
-exception Invalid_file_format
-
-let input_word ic =
-    let lo = input_byte ic in
-    let hi = input_byte ic in
-    (hi lsl 8) + lo
-
-let find_pe_header ic =
-    seek_in ic 0x3C;
-    let peheader = input_word ic in
-    seek_in ic peheader;
-    if input_char ic <> 'P' then
-        raise Invalid_file_format;
-    if input_char ic <> 'E' then
-        raise Invalid_file_format;
-    peheader
-
-let find_optional_header ic =
-    let peheader = find_pe_header ic in
-    let coffheader = peheader + 4 in
-    seek_in ic (coffheader + 16);
-    let optsize = input_word ic in
-    if optsize < 96 then
-        raise Invalid_file_format;
-    let optheader = coffheader + 20 in
-    seek_in ic optheader;
-    let magic = input_word ic in
-    if magic <> 0x010B && magic <> 0x020B then
-        raise Invalid_file_format;
-    optheader
-
-let change flag ic oc =
-    let optheader = find_optional_header ic in
-    seek_out oc (optheader + 64);
-    for i = 1 to 4 do
-        output_byte oc 0
-    done;
-    output_byte oc (if flag then 2 else 3)
-
-let usage () =
-  print_endline "Alters a Win32 executable file to use the Windows subsystem or not.";
-  print_endline "Usage: mkwinapp [-set|-unset] <filename>";
-  print_endline "Giving no option is equivalent to -set";
-  exit 1
-
-let main () =
-  let n = Array.length Sys.argv - 1 in
-  if not (n = 1 || n = 2) then usage ();
-  let flag =
-    if n = 1 then true
-    else if Sys.argv.(1) = "-set" then true
-    else if Sys.argv.(1) = "-unset" then false
-    else usage ()
-  in
-  let filename = Sys.argv.(n) in
-  let f = Unix.openfile filename [Unix.O_RDWR] 0 in
-  let ic = Unix.in_channel_of_descr f and oc = Unix.out_channel_of_descr f in
-  change flag ic oc
-
-let _ = main ()