Suppression du répertoire distrib: il fait désormais partie du projet coq-dev-tools sur GForge

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

30 files changed, 0 insertions, 2869 deletions

diff --git a/distrib/MacOS-X/Licence.rtf.template b/distrib/MacOS-X/Licence.rtf.template
deleted file mode 100644
index c0b43e7f03..0000000000
--- a/distrib/MacOS-X/Licence.rtf.template
+++ /dev/null
@@ -1,517 +0,0 @@
-{\rtf1\mac\ansicpg10000\cocoartf100
-{\fonttbl\f0\fswiss\fcharset77 Helvetica;}
-{\colortbl;\red255\green255\blue255;}
-\margl1440\margr1440\vieww9600\viewh15620\viewkind0
-\pard\tx1440\tx2880\tx4320\tx5760\tx7200\ql\qnatural
-
-\f0\fs24 \cf0 The source files of Coq VVERSION are released under the\
-terms of the GNU Less General Public Licence, version 2.1 (included\
-below), to the exception of some files located in the source\
-directories contrib/jprover and ide/utils that are released under the\
-terms of the GNU General Public Licence (see the corresponding files\
-for details).\
-\
-----------------------------------------------------------------------\
-                GNU LESSER GENERAL PUBLIC LICENSE\
-                       Version 2.1, February 1999\
-\
- Copyright (C) 1991, 1999 Free Software Foundation, Inc.\
-     59 Temple Place, Suite 330, Boston, MA  02111-1307  USA\
- Everyone is permitted to copy and distribute verbatim copies\
- of this license document, but changing it is not allowed.\
-\
-[This is the first released version of the Lesser GPL.  It also counts\
- as the successor of the GNU Library Public License, version 2, hence\
- the version number 2.1.]\
-\
-                            Preamble\
-\
-  The licenses for most software are designed to take away your\
-freedom to share and change it.  By contrast, the GNU General Public\
-Licenses are intended to guarantee your freedom to share and change\
-free software--to make sure the software is free for all its users.\
-\
-  This license, the Lesser General Public License, applies to some\
-specially designated software packages--typically libraries--of the\
-Free Software Foundation and other authors who decide to use it.  You\
-can use it too, but we suggest you first think carefully about whether\
-this license or the ordinary General Public License is the better\
-strategy to use in any particular case, based on the explanations below.\
-\
-  When we speak of free software, we are referring to freedom of use,\
-not price. Our General Public Licenses are designed to make sure that\
-you have the freedom to distribute copies of free software (and charge\
-for this service if you wish); that you receive source code or can get\
-it if you want it; that you can change the software and use pieces of\
-it in new free programs; and that you are informed that you can do\
-these things.\
-\
-  To protect your rights, we need to make restrictions that forbid\
-distributors to deny you these rights or to ask you to surrender these\
-rights.  These restrictions translate to certain responsibilities for\
-you if you distribute copies of the library or if you modify it.\
-\
-  For example, if you distribute copies of the library, whether gratis\
-or for a fee, you must give the recipients all the rights that we gave\
-you.  You must make sure that they, too, receive or can get the source\
-code.  If you link other code with the library, you must provide\
-complete object files to the recipients, so that they can relink them\
-with the library after making changes to the library and recompiling\
-it.  And you must show them these terms so they know their rights.\
-\
-  We protect your rights with a two-step method: (1) we copyright the\
-library, and (2) we offer you this license, which gives you legal\
-permission to copy, distribute and/or modify the library.\
-\
-  To protect each distributor, we want to make it very clear that\
-there is no warranty for the free library.  Also, if the library is\
-modified by someone else and passed on, the recipients should know\
-that what they have is not the original version, so that the original\
-author's reputation will not be affected by problems that might be\
-introduced by others.\
-\
-  Finally, software patents pose a constant threat to the existence of\
-any free program.  We wish to make sure that a company cannot\
-effectively restrict the users of a free program by obtaining a\
-restrictive license from a patent holder.  Therefore, we insist that\
-any patent license obtained for a version of the library must be\
-consistent with the full freedom of use specified in this license.\
-\
-  Most GNU software, including some libraries, is covered by the\
-ordinary GNU General Public License.  This license, the GNU Lesser\
-General Public License, applies to certain designated libraries, and\
-is quite different from the ordinary General Public License.  We use\
-this license for certain libraries in order to permit linking those\
-libraries into non-free programs.\
-\
-  When a program is linked with a library, whether statically or using\
-a shared library, the combination of the two is legally speaking a\
-combined work, a derivative of the original library.  The ordinary\
-General Public License therefore permits such linking only if the\
-entire combination fits its criteria of freedom.  The Lesser General\
-Public License permits more lax criteria for linking other code with\
-the library.\
-\
-  We call this license the "Lesser" General Public License because it\
-does Less to protect the user's freedom than the ordinary General\
-Public License.  It also provides other free software developers Less\
-of an advantage over competing non-free programs. These disadvantages\
-are the reason we use the ordinary General Public License for many\
-libraries.  However, the Lesser license provides advantages in certain\
-special circumstances.\
-\
-  For example, on rare occasions, there may be a special need to\
-encourage the widest possible use of a certain library, so that it\
-becomes a de-facto standard. To achieve this, non-free programs must\
-be allowed to use the library.  A more frequent case is that a free\
-library does the same job as widely used non-free libraries.  In this\
-case, there is little to gain by limiting the free library to free\
-software only, so we use the Lesser General Public License.\
-\
-  In other cases, permission to use a particular library in non-free\
-programs enables a greater number of people to use a large body of\
-free software.  For example, permission to use the GNU C Library in\
-non-free programs enables many more people to use the whole GNU\
-operating system, as well as its variant, the GNU/Linux operating\
-system.\
-\
-  Although the Lesser General Public License is Less protective of the\
-users' freedom, it does ensure that the user of a program that is\
-linked with the Library has the freedom and the wherewithal to run\
-that program using a modified version of the Library.\
-\
-  The precise terms and conditions for copying, distribution and\
-modification follow.  Pay close attention to the difference between a\
-"work based on the library" and a "work that uses the library".  The\
-former contains code derived from the library, whereas the latter must\
-be combined with the library in order to run.\
-\
-                  GNU LESSER GENERAL PUBLIC LICENSE\
-   TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION\
-\
-  0. This License Agreement applies to any software library or other\
-program which contains a notice placed by the copyright holder or\
-other authorized party saying it may be distributed under the terms of\
-this Lesser General Public License (also called "this License").\
-Each licensee is addressed as "you".\
-\
-  A "library" means a collection of software functions and/or data\
-prepared so as to be conveniently linked with application programs\
-(which use some of those functions and data) to form executables.\
-\
-  The "Library", below, refers to any such software library or work\
-which has been distributed under these terms.  A "work based on the\
-Library" means either the Library or any derivative work under\
-copyright law: that is to say, a work containing the Library or a\
-portion of it, either verbatim or with modifications and/or translated\
-straightforwardly into another language.  (Hereinafter, translation is\
-included without limitation in the term "modification".)\
-\
-  "Source code" for a work means the preferred form of the work for\
-making modifications to it.  For a library, complete source code means\
-all the source code for all modules it contains, plus any associated\
-interface definition files, plus the scripts used to control compilation\
-and installation of the library.\
-\
-  Activities other than copying, distribution and modification are not\
-covered by this License; they are outside its scope.  The act of\
-running a program using the Library is not restricted, and output from\
-such a program is covered only if its contents constitute a work based\
-on the Library (independent of the use of the Library in a tool for\
-writing it).  Whether that is true depends on what the Library does\
-and what the program that uses the Library does.\
-  \
-  1. You may copy and distribute verbatim copies of the Library's\
-complete source code as you receive it, in any medium, provided that\
-you conspicuously and appropriately publish on each copy an\
-appropriate copyright notice and disclaimer of warranty; keep intact\
-all the notices that refer to this License and to the absence of any\
-warranty; and distribute a copy of this License along with the\
-Library.\
-\
-  You may charge a fee for the physical act of transferring a copy,\
-and you may at your option offer warranty protection in exchange for a\
-fee.\
-\
-  2. You may modify your copy or copies of the Library or any portion\
-of it, thus forming a work based on the Library, and copy and\
-distribute such modifications or work under the terms of Section 1\
-above, provided that you also meet all of these conditions:\
-\
-    a) The modified work must itself be a software library.\
-\
-    b) You must cause the files modified to carry prominent notices\
-    stating that you changed the files and the date of any change.\
-\
-    c) You must cause the whole of the work to be licensed at no\
-    charge to all third parties under the terms of this License.\
-\
-    d) If a facility in the modified Library refers to a function or a\
-    table of data to be supplied by an application program that uses\
-    the facility, other than as an argument passed when the facility\
-    is invoked, then you must make a good faith effort to ensure that,\
-    in the event an application does not supply such function or\
-    table, the facility still operates, and performs whatever part of\
-    its purpose remains meaningful.\
-\
-    (For example, a function in a library to compute square roots has\
-    a purpose that is entirely well-defined independent of the\
-    application.  Therefore, Subsection 2d requires that any\
-    application-supplied function or table used by this function must\
-    be optional: if the application does not supply it, the square\
-    root function must still compute square roots.)\
-\
-These requirements apply to the modified work as a whole.  If\
-identifiable sections of that work are not derived from the Library,\
-and can be reasonably considered independent and separate works in\
-themselves, then this License, and its terms, do not apply to those\
-sections when you distribute them as separate works.  But when you\
-distribute the same sections as part of a whole which is a work based\
-on the Library, the distribution of the whole must be on the terms of\
-this License, whose permissions for other licensees extend to the\
-entire whole, and thus to each and every part regardless of who wrote\
-it.\
-\
-Thus, it is not the intent of this section to claim rights or contest\
-your rights to work written entirely by you; rather, the intent is to\
-exercise the right to control the distribution of derivative or\
-collective works based on the Library.\
-\
-In addition, mere aggregation of another work not based on the Library\
-with the Library (or with a work based on the Library) on a volume of\
-a storage or distribution medium does not bring the other work under\
-the scope of this License.\
-\
-  3. You may opt to apply the terms of the ordinary GNU General Public\
-License instead of this License to a given copy of the Library.  To do\
-this, you must alter all the notices that refer to this License, so\
-that they refer to the ordinary GNU General Public License, version 2,\
-instead of to this License.  (If a newer version than version 2 of the\
-ordinary GNU General Public License has appeared, then you can specify\
-that version instead if you wish.)  Do not make any other change in\
-these notices.\
-\
-  Once this change is made in a given copy, it is irreversible for\
-that copy, so the ordinary GNU General Public License applies to all\
-subsequent copies and derivative works made from that copy.\
-\
-  This option is useful when you wish to copy part of the code of\
-the Library into a program that is not a library.\
-\
-  4. You may copy and distribute the Library (or a portion or\
-derivative of it, under Section 2) in object code or executable form\
-under the terms of Sections 1 and 2 above provided that you accompany\
-it with the complete corresponding machine-readable source code, which\
-must be distributed under the terms of Sections 1 and 2 above on a\
-medium customarily used for software interchange.\
-\
-  If distribution of object code is made by offering access to copy\
-from a designated place, then offering equivalent access to copy the\
-source code from the same place satisfies the requirement to\
-distribute the source code, even though third parties are not\
-compelled to copy the source along with the object code.\
-\
-  5. A program that contains no derivative of any portion of the\
-Library, but is designed to work with the Library by being compiled or\
-linked with it, is called a "work that uses the Library".  Such a\
-work, in isolation, is not a derivative work of the Library, and\
-therefore falls outside the scope of this License.\
-\
-  However, linking a "work that uses the Library" with the Library\
-creates an executable that is a derivative of the Library (because it\
-contains portions of the Library), rather than a "work that uses the\
-library".  The executable is therefore covered by this License.\
-Section 6 states terms for distribution of such executables.\
-\
-  When a "work that uses the Library" uses material from a header file\
-that is part of the Library, the object code for the work may be a\
-derivative work of the Library even though the source code is not.\
-Whether this is true is especially significant if the work can be\
-linked without the Library, or if the work is itself a library.  The\
-threshold for this to be true is not precisely defined by law.\
-\
-  If such an object file uses only numerical parameters, data\
-structure layouts and accessors, and small macros and small inline\
-functions (ten lines or less in length), then the use of the object\
-file is unrestricted, regardless of whether it is legally a derivative\
-work.  (Executables containing this object code plus portions of the\
-Library will still fall under Section 6.)\
-\
-  Otherwise, if the work is a derivative of the Library, you may\
-distribute the object code for the work under the terms of Section 6.\
-Any executables containing that work also fall under Section 6,\
-whether or not they are linked directly with the Library itself.\
-\
-  6. As an exception to the Sections above, you may also combine or\
-link a "work that uses the Library" with the Library to produce a\
-work containing portions of the Library, and distribute that work\
-under terms of your choice, provided that the terms permit\
-modification of the work for the customer's own use and reverse\
-engineering for debugging such modifications.\
-\
-  You must give prominent notice with each copy of the work that the\
-Library is used in it and that the Library and its use are covered by\
-this License.  You must supply a copy of this License.  If the work\
-during execution displays copyright notices, you must include the\
-copyright notice for the Library among them, as well as a reference\
-directing the user to the copy of this License.  Also, you must do one\
-of these things:\
-\
-    a) Accompany the work with the complete corresponding\
-    machine-readable source code for the Library including whatever\
-    changes were used in the work (which must be distributed under\
-    Sections 1 and 2 above); and, if the work is an executable linked\
-    with the Library, with the complete machine-readable "work that\
-    uses the Library", as object code and/or source code, so that the\
-    user can modify the Library and then relink to produce a modified\
-    executable containing the modified Library.  (It is understood\
-    that the user who changes the contents of definitions files in the\
-    Library will not necessarily be able to recompile the application\
-    to use the modified definitions.)\
-\
-    b) Use a suitable shared library mechanism for linking with the\
-    Library.  A suitable mechanism is one that (1) uses at run time a\
-    copy of the library already present on the user's computer system,\
-    rather than copying library functions into the executable, and (2)\
-    will operate properly with a modified version of the library, if\
-    the user installs one, as long as the modified version is\
-    interface-compatible with the version that the work was made with.\
-\
-    c) Accompany the work with a written offer, valid for at\
-    least three years, to give the same user the materials\
-    specified in Subsection 6a, above, for a charge no more\
-    than the cost of performing this distribution.\
-\
-    d) If distribution of the work is made by offering access to copy\
-    from a designated place, offer equivalent access to copy the above\
-    specified materials from the same place.\
-\
-    e) Verify that the user has already received a copy of these\
-    materials or that you have already sent this user a copy.\
-\
-  For an executable, the required form of the "work that uses the\
-Library" must include any data and utility programs needed for\
-reproducing the executable from it.  However, as a special exception,\
-the materials to be distributed need not include anything that is\
-normally distributed (in either source or binary form) with the major\
-components (compiler, kernel, and so on) of the operating system on\
-which the executable runs, unless that component itself accompanies\
-the executable.\
-\
-  It may happen that this requirement contradicts the license\
-restrictions of other proprietary libraries that do not normally\
-accompany the operating system.  Such a contradiction means you cannot\
-use both them and the Library together in an executable that you\
-distribute.\
-\
-  7. You may place library facilities that are a work based on the\
-Library side-by-side in a single library together with other library\
-facilities not covered by this License, and distribute such a combined\
-library, provided that the separate distribution of the work based on\
-the Library and of the other library facilities is otherwise\
-permitted, and provided that you do these two things:\
-\
-    a) Accompany the combined library with a copy of the same work\
-    based on the Library, uncombined with any other library\
-    facilities.  This must be distributed under the terms of the\
-    Sections above.\
-\
-    b) Give prominent notice with the combined library of the fact\
-    that part of it is a work based on the Library, and explaining\
-    where to find the accompanying uncombined form of the same work.\
-\
-  8. You may not copy, modify, sublicense, link with, or distribute\
-the Library except as expressly provided under this License.  Any\
-attempt otherwise to copy, modify, sublicense, link with, or\
-distribute the Library is void, and will automatically terminate your\
-rights under this License.  However, parties who have received copies,\
-or rights, from you under this License will not have their licenses\
-terminated so long as such parties remain in full compliance.\
-\
-  9. You are not required to accept this License, since you have not\
-signed it.  However, nothing else grants you permission to modify or\
-distribute the Library or its derivative works.  These actions are\
-prohibited by law if you do not accept this License.  Therefore, by\
-modifying or distributing the Library (or any work based on the\
-Library), you indicate your acceptance of this License to do so, and\
-all its terms and conditions for copying, distributing or modifying\
-the Library or works based on it.\
-\
-  10. Each time you redistribute the Library (or any work based on the\
-Library), the recipient automatically receives a license from the\
-original licensor to copy, distribute, link with or modify the Library\
-subject to these terms and conditions.  You may not impose any further\
-restrictions on the recipients' exercise of the rights granted herein.\
-You are not responsible for enforcing compliance by third parties with\
-this License.\
-\
-  11. If, as a consequence of a court judgment or allegation of patent\
-infringement or for any other reason (not limited to patent issues),\
-conditions are imposed on you (whether by court order, agreement or\
-otherwise) that contradict the conditions of this License, they do not\
-excuse you from the conditions of this License.  If you cannot\
-distribute so as to satisfy simultaneously your obligations under this\
-License and any other pertinent obligations, then as a consequence you\
-may not distribute the Library at all.  For example, if a patent\
-license would not permit royalty-free redistribution of the Library by\
-all those who receive copies directly or indirectly through you, then\
-the only way you could satisfy both it and this License would be to\
-refrain entirely from distribution of the Library.\
-\
-If any portion of this section is held invalid or unenforceable under any\
-particular circumstance, the balance of the section is intended to apply,\
-and the section as a whole is intended to apply in other circumstances.\
-\
-It is not the purpose of this section to induce you to infringe any\
-patents or other property right claims or to contest validity of any\
-such claims; this section has the sole purpose of protecting the\
-integrity of the free software distribution system which is\
-implemented by public license practices.  Many people have made\
-generous contributions to the wide range of software distributed\
-through that system in reliance on consistent application of that\
-system; it is up to the author/donor to decide if he or she is willing\
-to distribute software through any other system and a licensee cannot\
-impose that choice.\
-\
-This section is intended to make thoroughly clear what is believed to\
-be a consequence of the rest of this License.\
-\
-  12. If the distribution and/or use of the Library is restricted in\
-certain countries either by patents or by copyrighted interfaces, the\
-original copyright holder who places the Library under this License may add\
-an explicit geographical distribution limitation excluding those countries,\
-so that distribution is permitted only in or among countries not thus\
-excluded.  In such case, this License incorporates the limitation as if\
-written in the body of this License.\
-\
-  13. The Free Software Foundation may publish revised and/or new\
-versions of the Lesser General Public License from time to time.\
-Such new versions will be similar in spirit to the present version,\
-but may differ in detail to address new problems or concerns.\
-\
-Each version is given a distinguishing version number.  If the Library\
-specifies a version number of this License which applies to it and\
-"any later version", you have the option of following the terms and\
-conditions either of that version or of any later version published by\
-the Free Software Foundation.  If the Library does not specify a\
-license version number, you may choose any version ever published by\
-the Free Software Foundation.\
-\
-  14. If you wish to incorporate parts of the Library into other free\
-programs whose distribution conditions are incompatible with these,\
-write to the author to ask for permission.  For software which is\
-copyrighted by the Free Software Foundation, write to the Free\
-Software Foundation; we sometimes make exceptions for this.  Our\
-decision will be guided by the two goals of preserving the free status\
-of all derivatives of our free software and of promoting the sharing\
-and reuse of software generally.\
-\
-                            NO WARRANTY\
-\
-  15. BECAUSE THE LIBRARY IS LICENSED FREE OF CHARGE, THERE IS NO\
-WARRANTY FOR THE LIBRARY, TO THE EXTENT PERMITTED BY APPLICABLE LAW.\
-EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR\
-OTHER PARTIES PROVIDE THE LIBRARY "AS IS" WITHOUT WARRANTY OF ANY\
-KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE\
-IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR\
-PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE\
-LIBRARY IS WITH YOU.  SHOULD THE LIBRARY PROVE DEFECTIVE, YOU ASSUME\
-THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.\
-\
-  16. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN\
-WRITING WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY\
-AND/OR REDISTRIBUTE THE LIBRARY AS PERMITTED ABOVE, BE LIABLE TO YOU\
-FOR DAMAGES, INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR\
-CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THE\
-LIBRARY (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING\
-RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR A\
-FAILURE OF THE LIBRARY TO OPERATE WITH ANY OTHER SOFTWARE), EVEN IF\
-SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH\
-DAMAGES.\
-\
-                     END OF TERMS AND CONDITIONS\
-\
-           How to Apply These Terms to Your New Libraries\
-\
-  If you develop a new library, and you want it to be of the greatest\
-possible use to the public, we recommend making it free software that\
-everyone can redistribute and change.  You can do so by permitting\
-redistribution under these terms (or, alternatively, under the terms of the\
-ordinary General Public License).\
-\
-  To apply these terms, attach the following notices to the library.  It is\
-safest to attach them to the start of each source file to most effectively\
-convey the exclusion of warranty; and each file should have at least the\
-"copyright" line and a pointer to where the full notice is found.\
-\
-    <one line to give the library's name and a brief idea of what it does.>\
-    Copyright (C) <year>  <name of author>\
-\
-    This library is free software; you can redistribute it and/or\
-    modify it under the terms of the GNU Lesser General Public\
-    License as published by the Free Software Foundation; either\
-    version 2.1 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\
-    Lesser General Public License for more details.\
-\
-    You should have received a copy of the GNU Lesser General Public\
-    License along with this library; if not, write to the Free Software\
-    Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA\
-\
-Also add information on how to contact you by electronic and paper mail.\
-\
-You should also get your employer (if you work as a programmer) or your\
-school, if any, to sign a "copyright disclaimer" for the library, if\
-necessary.  Here is a sample; alter the names:\
-\
-  Yoyodyne, Inc., hereby disclaims all copyright interest in the\
-  library `Frob' (a library for tweaking knobs) written by James Random Hacker.\
-\
-  <signature of Ty Coon>, 1 April 1990\
-  Ty Coon, President of Vice\
-\
-That's all there is to it!\
-}\
diff --git a/distrib/MacOS-X/ReadMe.rtf.template b/distrib/MacOS-X/ReadMe.rtf.template
deleted file mode 100644
index 2878e1c4d2..0000000000
--- a/distrib/MacOS-X/ReadMe.rtf.template
+++ /dev/null
@@ -1,32 +0,0 @@
-{\rtf1\mac\ansicpg10000\cocoartf100
-{\fonttbl\f0\fswiss\fcharset77 Helvetica;}
-{\colortbl;\red255\green255\blue255;}
-\margl1440\margr1440\vieww9000\viewh9000\viewkind0
-\pard\tx1440\tx2880\tx4320\tx5760\tx7200\ql\qnatural
-
-\f0\fs24 \cf0 Developed in the LogiCal project, the Coq tool is a formal\
-proof management system: a proof done with Coq is mechanically\
-checked by the machine. In particular, Coq allows:\
-\
-- the definition of functions or predicates,\
-- to state mathematical theorems and software specifications,\
-- to develop interactively formal proofs of these theorems,\
-- to check these proofs by a small certification "kernel".\
-\
-Coq is based on a logical framework called "Calculus of Inductive\
-Constructions" extended by a modular development system for\
-theories.\
-\
-Coq also includes\
-\
-- a mechanism for automatic generation of certified programs\
-  from proofs of their specifications\
-- a graphical user interface based on gtk (CoqIde)\
-  [not included in this package]\
-- a documentation tool (coqdoc)\
-- dependency and makefile generation tools for Coq (coq_makefile\
-  and coqdep)\
-- a preprocessor for TeX files that include Coq commands (coq-tex)\
-\
-Coq is written in the Objective Caml language.\
-}
diff --git a/distrib/MacOS-X/Welcome.rtf.template b/distrib/MacOS-X/Welcome.rtf.template
deleted file mode 100644
index 8925f1dfb5..0000000000
--- a/distrib/MacOS-X/Welcome.rtf.template
+++ /dev/null
@@ -1,10 +0,0 @@
-{\rtf1\mac\ansicpg10000\cocoartf100
-{\fonttbl\f0\fswiss\fcharset77 Helvetica;}
-{\colortbl;\red255\green255\blue255;}
-\margl1440\margr1440\vieww9000\viewh9000\viewkind0
-\pard\tx1440\tx2880\tx4320\tx5760\tx7200\ql\qnatural
-
-\f0\fs24 \cf0 This package will install the MacOS X binary distribution of Coq VVERSION.\
-\
-You will need about 30MB of disk space to install this package.\
-}
diff --git a/distrib/MacOS-X/coq.info.template b/distrib/MacOS-X/coq.info.template
deleted file mode 100644
index e32b329091..0000000000
--- a/distrib/MacOS-X/coq.info.template
+++ /dev/null
@@ -1,15 +0,0 @@
-Title Coq
-Version VERSION
-Description The Coq proof assistant
-DefaultLocation /
-DeleteWarning 
-
-### Package Flags
-
-NeedsAuthorization YES
-Required NO
-Relocatable NO
-RequiresReboot NO
-UseUserMask NO
-OverwritePermissions NO
-InstallFat NO
diff --git a/distrib/MacOS-X/package b/distrib/MacOS-X/package
deleted file mode 100755
index 5bc7d84909..0000000000
--- a/distrib/MacOS-X/package
+++ /dev/null
@@ -1,274 +0,0 @@
-#! /bin/csh -ef
-
-# This is a copy of MacOS 10.2 "package" script (it disappeared in MacOS 10.3!)
-
-set prog = `/usr/bin/basename $0`
-set usage = "Usage: $prog [-f] root-dir info-file [tiff-file] [-d dest-dir] [-r resource-dir] [-traditional | -gnutar]"
-set noglob
-
-if (-x /usr/bin/mkbom) then
-    set mkbom=/usr/bin/mkbom
-    set lsbom=/usr/bin/lsbom
-else
-    set mkbom=/usr/etc/mkbom
-    set lsbom=/usr/etc/lsbom
-endif
-
-if (-x /usr/bin/awk) then
-    set awk=/usr/bin/awk
-else
-    set awk=/bin/awk
-endif
-
-set gnutar=/usr/bin/gnutar
-set tar=/usr/bin/tar
-set pax=/bin/pax
-
-# gather parameters
-if ($#argv == 0) then
-    echo $usage
-    exit(1)
-endif
-
-while ( $#argv > 0 )
-    switch ( $argv[1] )
-	case -d:
-	    if ( $?destDir ) then
-		echo ${prog}: dest-dir parameter already set to ${destDir}.
-		echo $usage
-		exit(1)
-	    else if ( $#argv < 2 ) then
-		echo ${prog}: -d option requires destination directory.
-		echo $usage
-		exit(1)
-	    else
-		set destDir = $argv[2]
-		shift; shift
-		breaksw
-	    endif
-	case -f:
-	    if ( $?rootDir ) then
-		echo ${prog}: root-dir parameter already set to ${rootDir}.
-		echo $usage
-		exit(1)
-	    else if ( $#argv < 2 ) then
-		echo ${prog}: -f option requires package root directory.
-		echo $usage
-		exit(1)
-	    else
-		set rootDir = $argv[2]
-		set fflag
-		shift; shift
-		breaksw
-	    endif
-	case -r:
-	    if ( $?resDir ) then
-		echo ${prog}: resource-dir parameter already set to ${resDir}.
-		echo $usage
-		exit(1)
-	    else if ( $#argv < 2 ) then
-		echo ${prog}: -r option requires package resource directory.
-		echo $usage
-		exit(1)
-	    else
-		set resDir = $argv[2]
-		shift; shift
-		breaksw
-	    endif
-	case -traditional:
-	    set usetar
-            unset usegnutar
-	    unset usepax
-	    breaksw
-        case -gnutar:
-	    set usegnutar
-            unset usepax
-	    unset usetar
-	case -B:
-	    # We got long file names, better use bigtar instead
-	    #set archiver = /NextAdmin/Installer.app/Resources/installer_bigtar
-	    echo 2>&1 ${prog}: -B flag is no longer relevant.
-	    shift
-	    breaksw
-	case -*:
-	    echo ${prog}: Unknown option: $argv[1]
-	    echo $usage
-	    exit(1)
-	case *.info:
-	    if ( $?info ) then
-		echo ${prog}: info-file parameter already set to ${info}.
-		echo $usage
-		exit(1)
-	    else
-		set info = "$argv[1]"
-		shift
-		breaksw
-	    endif
-	case *.tiff:
-	    if ( $?tiff ) then
-		echo ${prog}: tiff-file parameter already set to ${tiff}.
-		echo $usage
-		exit(1)
-	    else
-		set tiff = "$argv[1]"
-		shift
-		breaksw
-	    endif
-	default:
-	    if ( $?rootDir ) then
-		echo ${prog}: unrecognized parameter: $argv[1]
-		echo $usage
-		exit(1)
-	    else
-		set rootDir = "$argv[1]"
-		shift
-		breaksw
-	    endif
-    endsw
-end
-
-# check for mandatory parameters
-if ( ! $?rootDir ) then
-    echo ${prog}: missing root-dir parameter.
-    echo $usage
-    exit(1)
-else if ( ! $?info) then
-    echo ${prog}: missing info-file parameter.
-    echo $usage
-    exit(1)
-endif
-
-# destDir gets default value if unset on command line
-if ( $?destDir ) then
-    /bin/mkdir -p $destDir
-else
-    set destDir = .
-endif
-
-# derive the root name for the package from the root name of the info file
-set root = `/usr/bin/basename $info .info`
-
-# create package directory
-set pkg = ${destDir}/${root}.pkg
-echo Generating Installer package $pkg ...
-if ( -e $pkg ) /bin/rm -rf $pkg
-/bin/mkdir -p -m 755 $pkg
-
-# (gnu)tar/pax and compress root directory to package archive
-echo -n "	creating package archive ... "
-if ( $?fflag ) then
-    set pkgTop = ${rootDir:t}
-    set parent = ${rootDir:h}
-    if ( "$parent" == "$pkgTop" ) set parent = "."
-else
-    set parent = $rootDir
-    set pkgTop = .    
-endif
-if ( $?usetar ) then
-    set pkgArchive = $pkg/$root.tar.Z
-    (cd $parent; $tar -w $pkgTop) | /usr/bin/compress -f -c > $pkgArchive
-else if ( $?usegnutar ) then
-    set pkgArchive = $pkg/$root.tar.gz
-    (cd $parent; $gnutar zcf $pkgArchive $pkgTop)
-else
-    set pkgArchive = $pkg/$root.pax.gz
-    (cd $parent; $pax -w -z -x cpio $pkgTop) > $pkgArchive
-endif
-/bin/chmod 444 $pkgArchive
-echo done.
-
-# copy info file to package
-set pkgInfo = $pkg/$root.info
-echo -n "	copying ${info:t} ... "
-/bin/cp $info $pkgInfo
-/bin/chmod 444 $pkgInfo
-echo done.
-
-# copy tiff file to package
-if ( $?tiff ) then
-    set pkgTiff = $pkg/$root.tiff
-    echo -n "	copying ${tiff:t} ... "
-    /bin/cp $tiff $pkgTiff
-    /bin/chmod 444 $pkgTiff
-    echo done.
-endif
-
-# copy resources to package
-if ( $?resDir ) then
-    echo -n "	copying ${resDir:t} ... "
-
-    # don't want to see push/pop output
-    pushd $resDir > /dev/null
-	# get lists of resources. We'll want to change
-	# permissions on just these things later.
-        set directoriesInResDir = `find . -type d`
-        set filesInResDir = `find . -type f`
-    popd > /dev/null
-
-    # copy the resource directory contents into the package directory
-    foreach resFile (`ls $resDir`)
-	cp -r $resDir/$resFile $pkg
-    end
-
-    pushd $pkg > /dev/null
-	# Change all directories to +r+x, except the package
-	# directory itself
-        foreach resFileItem ($directoriesInResDir)
-            if ( $resFileItem != "." ) then
-                chmod 555 $resFileItem
-            endif
-        end
-	# change all flat files to read only
-        foreach resFileItem ($filesInResDir)
-            chmod 444 $resFileItem
-        end
-    popd > /dev/null
-
-    echo done.
-endif
-
-# generate bom file
-set pkgBom = $pkg/$root.bom
-echo -n "	generating bom file ... "
-/bin/rm -f $pkgBom
-if ( $?fflag ) then
-    $mkbom $parent $pkgBom >& /dev/null
-else
-    $mkbom $rootDir $pkgBom >& /dev/null
-endif
-/bin/chmod 444 $pkgArchive
-echo done.
-	
-# generate sizes file
-set pkgSizes = $pkg/$root.sizes
-echo -n "	generating sizes file ... "
-
-# compute number of files in package
-set numFiles = `$lsbom -s $pkgBom | /usr/bin/wc -l`
-
-# compute package size when compressed
-@ compressedSize = `/usr/bin/du -k -s $pkg | $awk '{print $1}'`
-@ compressedSize += 3		# add 1KB each for sizes, location, status files
-
-@ infoSize = `/bin/ls -s $pkgInfo | $awk '{print $1}'`
-@ bomSize = `/bin/ls -s $pkgBom | $awk '{print $1}'`
-if ( $?tiff ) then
-    @ tiffSize = `/bin/ls -s $pkgTiff | $awk '{print $1}'`
-else
-    @ tiffSize = 0
-endif 
-
-@ installedSize = `/usr/bin/du -k -s $rootDir | $awk '{print $1}'`
-@ installedSize += $infoSize + $bomSize + $tiffSize + 3
-
-# echo size parameters to sizes file
-echo NumFiles $numFiles             >  $pkgSizes
-echo InstalledSize $installedSize   >> $pkgSizes
-echo CompressedSize $compressedSize >> $pkgSizes
-echo done.
-echo " ... finished generating $pkg."
-
-exit(0)
-
-# end package
-	
diff --git a/distrib/Makefile b/distrib/Makefile
deleted file mode 100644
index 91f8b3fbc4..0000000000
--- a/distrib/Makefile
+++ /dev/null
@@ -1,482 +0,0 @@
-# Building the different files of the coq distribution
-
-# Rk: parameterized targets are not accepted on DEC boxes...
-
-# config.distrib defines: VERSION, PREVIOUSVERSION, DISTRIBDIR,
-# CVSMODULE, CVSTAG, RELEASENUM and ARCH 
-sinclude config.distrib
-LOCALARCH=`uname -m`
-SYSTEM=`uname -s`
-
-BUILDTARGET=world
-INSTTARGET=install
-MAKECOQ=make
-
-# We assume we are not on pauillac, so we use ssh and scp
-SERVER=pauillac.inria.fr
-CP=scp -p
-SERVEREXEC=ssh $(SERVER) sh -c
-FTPDIR=/net/pauillac/infosystems/ftp/coq/coq
-#WWWDIR=/net/pauillac/infosystems/www/coq
-
-FTPVDIR=$(SERVER):$(FTPDIR)/V$(VERSION)
-
-######################
-
-noarguments:
-	@echo Please use either
-	@echo "make tag          to tag the current archive with the release number"
-	@echo "make tar-gz       to build a tar.gz of sources"
-	@echo "make arch-tar-gz  to prepare a binary tar.gz for this arch"
-	@echo "make rpm          to prepare source and arch rpms"
-	@echo "make src-rpm      to prepare source rpms from the tar.gz"
-	@echo "make arch-rpm     to prepare binary rpms for the current arch from the src.rpm"
-	@echo "make ide-rpm      to build a src.rpm and a rpm for coqide on this arch"
-	@echo "make ide-arch-rpm to build a rpm for coqide on this arch from the src.rpm"
-	@echo "make pcoq-rpm     to build a src.rpm and a rpm for pcoq on this arch"
-	@echo "make deb          to build a debian package"
-	@echo "make win          to build a windows package"
-	@echo "make windows-installer to build a windows install program"
-	@echo "make macosx       to build a MacOS-X package on a disk image"
-	@echo "make contrib-tag     to tag the current contrib state with the release number"
-	@echo "make contrib-tar-gz  to build a tar.gz of contrib sources"
-	@echo "make ftp-install     to prepare the ftp repository and copy the packages done"
-	@echo "make tar-gz-ftp-install         |add the corresponding"
-	@echo "make src-rpm-ftp-install        |packages to the ftp"
-	@echo "make arch-rpm-ftp-install       |repository supposed"
-	@echo "make arch-tar-gz-ftp-install    |to be already"
-	@echo "make contrib-ftp-install	       |prepared"
-	@echo
-	@echo "make clean        to remove temporary files"
-	@echo "make cleanall     also removes built packages" 
-
-################## Main targets
-
-COQPACKAGE=coq-$(VERSION)
-
-distrib: tag tar-gz
-
-###################################################################
-# Tagging the archive
-#
-
-tag:
-	echo -n "Tagging the archive with version number $(CVSTAG)...";\
-	cvs rtag -F $(CVSTAG) $(CVSMODULE)
-
-
-## Use make LOCAL=1 to build packages from working directory...
-ifeq ($(LOCAL),1)
-# export sources of the current work directory
-WORKDIR=..
-$(COQPACKAGE):
-	@echo "Copying sources from work directory"
-	@- rm -rf $(COQPACKAGE)
-	mkdir $(COQPACKAGE)
-	cd $(WORKDIR) ; cp -rf `ls -a | egrep -v 'distrib|^\.$$|^\.\.$$'` $(DISTRIBDIR)/$(COQPACKAGE)/
-	cd $(COQPACKAGE)/ ; $(MAKECOQ) clean; \
-	  rm -fr CVS */CVS */*/CVS */*/*/CVS */*/*/*/CVS
-	find $(COQPACKAGE) -name CVS -type d -exec rm -fr {} \;
-else
-# export a fresh copy of the tagged CVS version
-$(COQPACKAGE):
-	@echo -n Exporting a fresh copy of the archive...
-	@- rm -rf $(COQPACKAGE)
-	@cvs export -d $(COQPACKAGE) -r $(CVSTAG) $(CVSMODULE)
-	@echo done
-endif
-
-###################################################################
-# .tar.gz packages (sources, binaries)
-#
-
-TARGZ=$(COQPACKAGE).tar.gz
-ARCHTAR=$(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar
-ARCHTARGZ=$(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar.gz
-
-tar-gz:
-	rm -f $(TARGZ)
-	$(MAKE) $(TARGZ)
-
-$(TARGZ): $(COQPACKAGE)
-	@rm -rf $(COQPACKAGE)/doc     # doc is implementation doc
-	@rm -rf $(COQPACKAGE)/distrib
-	@rm -rf $(COQPACKAGE)/KNOWN-BUGS
-	@rm -rf $(COQPACKAGE)/{TODO,ANNONCE,PROBLEMES}
-	@rm -rf $(COQPACKAGE)/theories/Num
-	@rm -rf $(COQPACKAGE)/contrib/graphs
-	@rm -rf $(COQPACKAGE)/doc/newsyntax.tex 
-	@rm -f $(COQPACKAGE)/make.result
-	@rm -rf $(COQPACKAGE)/test-suite/parser   # tests pcoq
-	@find $(COQPACKAGE) -name ".cvsignore" -exec rm {} \;
-	@echo done
-	@echo -n Building the tar.gz source package
-	@tar cvf $(COQPACKAGE).tar $(COQPACKAGE)
-	@gzip --best --force $(COQPACKAGE).tar
-	@chmod g+w $(TARGZ)
-	@echo done
-	@echo Checking release parameters
-	./check-list
-	@echo done
-
-test:
-	- rm -rf $(COQPACKAGE)
-	gunzip -c $(TARGZ) > tmp.tar
-	tar xf tmp.tar
-	rm -f tmp.tar
-	@echo Trying "$(MAKECOQ) $(BUILDTARGET) check"
-	(cd $(COQPACKAGE);\
-	 ./configure -local -opt -emacs emacs;\
-	 $(MAKECOQ) world check >& test.log;\
-	 if [ $$? = 0 ];\
-	 then echo '"$(MAKECOQ) $(BUILDTARGET) check" succeeded';\
-	 else echo '"$(MAKECOQ) $(BUILDTARGET) check" failed'; exit 1;\
-	 fi)
-	@echo "Compilation succeeded"
-
-# where binaries are compiled
-ARCHBUILDROOT=$(DISTRIBDIR)/tar-$(ARCH)
-ARCHINSTALL=$(ARCHBUILDROOT)/buildroot
-
-arch-tar-gz:
-	$(MAKE) arch-image
-	$(MAKE) arch-tar-gz-final
-
-arch-image: $(TARGZ)
-	@echo "Building $(ARCHTARGZ) to be installed in /usr/local/"
-	@echo "Warning: leading / is removed"
-	@-rm -fr $(ARCHINSTALL) $(ARCHBUILDROOT)
-	@mkdir -p $(ARCHBUILDROOT) $(ARCHINSTALL)
-	@echo "Building binaries... (see arch-image.log)"
-	(cd $(ARCHBUILDROOT);\
-	 gunzip -c $(DISTRIBDIR)/$(TARGZ) | tar xf -;\
-	 cd $(COQPACKAGE);\
-	 ./configure -prefix /usr/local -emacslib /usr/local/lib/emacs/site-lisp -opt -reals all;\
-	 $(MAKECOQ) coq check;\
-	 $(MAKECOQ) -e COQINSTALLPREFIX=$(ARCHINSTALL) BASETEXDIR=$(ARCHINSTALL) install-coq) > arch-image.log 2>&1
-	@echo " .... done"
-
-arch-tar-gz-final:
-	(cd $(ARCHBUILDROOT)/buildroot;\
-	 tar -cvf $(DISTRIBDIR)/$(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar *)
-	gzip --best $(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar
-	chmod g+w $(ARCHTARGZ)
-
-clean::
-	rm -fr $(ARCHINSTALL) $(ARCHBUILDROOT)
-
-cleanall::
-	rm -f $(COQPACKAGE) $(TARGZ) $(ARCHTARGZ) arch-image.log test.log
-
-###################################################################
-# RPM (Coq, CoqIde and Pcoq are separated)
-#
-rpm: src-rpm arch-rpm
-src-rpm: coq-src-rpm ide-src-rpm pcoq-src-rpm
-arch-rpm: coq-arch-rpm ide-arch-rpm pcoq-arch-rpm
-
-coq-rpm: coq-src-rpm coq-arch-rpm
-ide-rpm: ide-src-rpm ide-arch-rpm
-pcoq-rpm: pcoq-src-rpm pcoq-arch-rpm
-
-RPMTOPDIR=$(DISTRIBDIR)/RH/src
-RPMTMPPATHDIR=$(RPMTOPDIR)/admin
-RPMBUILDROOT=$(RPMTOPDIR)/install
-
-# rpm versions 2 and 3: replace rpmbuild by rpm 
-RAWRPM=rpmbuild
-RPMVERSION=`$(RAWRPM) --version | sed -e "s/RPM version \(.\).*/\1/"`
-
-# option --target avoids problem with i386/i686
-RPM=$(RAWRPM) --buildroot $(RPMBUILDROOT) --target $(ARCH) --rcfile RH/rpmrc
-
-# rpm files
-RPMEXT=$(VERSION)-$(RELEASENUM)
-COQRPMPACKAGE=coq-$(RPMEXT)
-COQIDERPMPACKAGE=coqide-$(RPMEXT)
-PCOQRPMPACKAGE=coq_ext_for_pcoq-$(RPMEXT)
-COQSRCRPM=$(COQRPMPACKAGE).src.rpm
-COQRPM=$(COQRPMPACKAGE).$(ARCH).rpm
-COQIDESRCRPM=$(COQIDERPMPACKAGE).src.rpm
-COQIDERPM=$(COQIDERPMPACKAGE).$(ARCH).rpm
-PCOQSRCRPM=$(PCOQRPMPACKAGE).src.rpm
-PCOQRPM=$(PCOQRPMPACKAGE).$(ARCH).rpm
-
-RPMLOG=$(DISTRIBDIR)/RH/rpm.log
-RPMFILESLOG=$(DISTRIBDIR)/RH/coqfiles.log
-
-coq-src-rpm: $(COQSRCRPM)
-coq-arch-rpm: $(COQRPM)
-
-ide-src-rpm: $(COQIDESRCRPM)
-ide-arch-rpm: $(COQIDERPM)
-
-pcoq-src-rpm: $(PCOQSRCRPM)
-pcoq-arch-rpm: $(PCOQRPM)
-
-$(RPMTOPDIR):
-	@mkdir -p $(RPMTOPDIR)/BUILD
-	@mkdir -p $(RPMTOPDIR)/RPMS
-	@mkdir -p $(RPMTOPDIR)/SOURCES
-	@mkdir -p $(RPMTOPDIR)/SPECS
-	@mkdir -p $(RPMTOPDIR)/SRPMS
-	@mkdir -p $(RPMTMPPATHDIR)
-	@mkdir -p $(RPMTOPDIR)/RPMS/$(ARCH)
-
-RH/rpmrc: config.distrib $(RPMTOPDIR)
-	(if [ "$(RPMVERSION)" != "2" ];\
-	then\
-	echo %_topdir $(RPMTOPDIR) > RH/rpmmacros;\
-	echo %_tmppath $(RPMTMPPATHDIR) >> RH/rpmmacros;\
-	echo %_arch $(ARCH) >> RH/rpmmacros;\
-	echo macrofiles:/usr/lib/rpm/macros:RH/rpmmacros > RH/rpmrc;\
-	else\
-	echo topdir: $(RPMTOPDIR) > RH/rpmrc;\
-	echo tmppath: $(RPMTMPPATHDIR) >> RH/rpmrc;\
-	fi)
-
-%-$(RPMEXT).src.rpm: RH/%.spec $(TARGZ) RH/rpmrc
-	cp -f petit-coq.gif $(RPMTOPDIR)/SOURCES
-	cp -f $(TARGZ) $(RPMTOPDIR)/SOURCES
-	$(RPM) -bs RH/$*.spec
-	mv $(RPMTOPDIR)/SRPMS/$@ .
-	chmod g+w $@
-
-%.$(ARCH).rpm: %.src.rpm
-	@mkdir -p $(RPMBUILDROOT)
-	@echo "Building the $(ARCH) rpm for $*... (see RH/rpm.log)"
-	$(RPM) --rebuild $< > $(RPMLOG)
-	mv $(RPMTOPDIR)/RPMS/$(ARCH)/$@ .
-	chmod g+w $@
-
-clean::
-	rm -fr $(RPMTOPDIR) RH/rpmmacros RH/rpmrc
-
-cleanall::
-	rm -f *.rpm $(RPMLOG) $(RPMFILESLOG)
-
-###################################################################
-# Zip for Windows (package does not contain coqide)
-#
-
-COQWINZIP=$(COQPACKAGE)-Win.zip
-WINBUILDROOT=$(DISTRIBDIR)/winbuildroot
-WININSTALL=$(DISTRIBDIR)/wininstallroot
-
-
-win: $(COQWINZIP)
-
-$(COQWINZIP): $(TARGZ)
-	@echo "Building $(COQWINZIP) to be installed in \coq\bin"
-	@echo "Warning: leading / is removed"
-	@-rm -fr $(WINBUILDROOT) $(WININSTALL)
-	@-mkdir -p $(WINBUILDROOT) $(WININSTALL)
-	@echo "Compiling and installing coq... (see win.log)"
-	(cd $(WINBUILDROOT);\
-	 gunzip -c $(DISTRIBDIR)/$(TARGZ) | tar xf -;\
-	 cd $(COQPACKAGE);\
-	 ./configure -bindir /coq/bin -libdir /coq/lib -mandir /coq/man -emacslib /coq/emacs -reals all -coqide no;\
-	 $(MAKECOQ) coq;\
-	 $(MAKECOQ) -e COQINSTALLPREFIX=$(WININSTALL) BASETEXDIR=$(WININSTALL) install-coq) > win.log
-	mv $(WINBUILDROOT)/$(COQPACKAGE)/INSTALL.win $(WININSTALL)/INSTALL.txt
-	cd $(WININSTALL); zip -A -r $(DISTRIBDIR)/$(COQWINZIP) *
-
-#################################
-# Windows installer
-# Needs Nsis http://nsis.sourceforge.net/Main_Page
-#################################
-
-MAKENSIS = "/cygdrive/c/Program Files/NSIS/makensis.exe"
-WIN_INSTALLER:= $(COQPACKAGE)-installer.exe
-
-windows-installer: $(WIN_INSTALLER)
-
-$(WIN_INSTALLER): 
-	@echo "Building Coq."
-	cd ..;./configure -prefix /coq -emacslib /coq/emacs -reals all;make world #Prefix is not used in fact.
-	@echo "Building the windows installer."
-	$(MAKENSIS) /DMY_VERSION=$(VERSION) /DOUTFILE=$(WIN_INSTALLER) windows/coq.nsi
-
-clean::
-	rm -fr $(WINBUILDROOT) $(WININSTALL)
-
-cleanall::
-	rm -f $(COQWINZIP) win.log
-
-###################################################################
-# Debian
-#
-
-COQDEBPACKAGE=coq_$(VERSION)-$(RELEASENUM)_i386.deb
-COQDEBCHANGES=coq_$(VERSION)-$(RELEASENUM)_*.changes
-COQDEBORIG=coq_$(VERSION).orig
-COQDEBTARGZ=$(COQDEBORIG).tar.gz
-COQIDEDEBPACKAGE=coqide_$(VERSION)-$(RELEASENUM)_i386.deb
-
-DEBIANBUILD=$(DISTRIBDIR)/deb/build
-DEBIANLOG=$(DISTRIBDIR)/deb/deb.log
-LINTIANLOG=$(DISTRIBDIR)/deb/lintian.log
-
-deb: prep-deb
-	cd $(DEBIANBUILD)/$(COQPACKAGE) ;\
-	 dpkg-buildpackage -rfakeroot -uc -us 2>&1 | tee $(DEBIANLOG)
-	(lintian $(DEBIANBUILD)/$(COQDEBCHANGES) | tee $(LINTIANLOG)) || true
-
-$(COQDEBTARGZ): $(TARGZ)
-	tar xzf $(TARGZ)
-	mv $(COQPACKAGE) $(COQDEBORIG)
-	tar czf $(COQDEBTARGZ) $(COQDEBORIG)	
-	rm -rf $(COQDEBORIG)
-
-prep-deb: $(COQDEBTARGZ) $(TARGZ)
-	@rm -rf $(DEBIANBUILD)
-	@mkdir -p $(DEBIANBUILD)
-	cp $(COQDEBTARGZ) $(DEBIANBUILD)
-	cd $(DEBIANBUILD) ; tar xzf $(DISTRIBDIR)/$(TARGZ)
-	cp -a debian $(DEBIANBUILD)/$(COQPACKAGE)
-	rm -rf $(DEBIANBUILD)/$(COQPACKAGE)/debian/CVS
-	date > prep-deb
-
-deb-sign: prep-deb
-	cd $(DEBIANBUILD)/$(COQPACKAGE) ;\
-	 dpkg-buildpackage -rfakeroot 2>&1 | tee $(DEBIANLOG)
-	(lintian $(DEBIANBUILD)/$(COQDEBCHANGES) | tee $(LINTIANLOG)) || true
-
-
-clean::
-	rm -fr $(DEBIANBUILD)
-
-cleanall::
-	rm -f $(DEBIANLOG) $(LINTIANLOG)
-
-###################################################################
-# Mac OS X
-#
-
-MACOSXPKG=coq-$(VERSION).pkg
-MACOSXDMG=coq-$(VERSION)-macosx.dmg
-
-macosx:
-	# Builds the /usr/local/bin image
-	$(MAKE) arch-image
-	# Builds the pkg file
-	$(MAKE) macosx-pkg
-	$(MAKE) macosx-dmg
-
-macosx-pkg:
-	# Builds the info file
-	sed -e "s/VERSION/$(VERSION)/g" MacOS-X/coq.info.template > MacOS-X/coq-$(VERSION).info
-	# Builds the resources files
-	rm -rf MacOS-X/Resources
-	mkdir MacOS-X/Resources
-	sed -e "s/VERSION/$(VERSION)/g" MacOS-X/Licence.rtf.template > MacOS-X/Resources/License.rtf
-	sed -e "s/VERSION/$(VERSION)/g" MacOS-X/Welcome.rtf.template > MacOS-X/Resources/Welcome.rtf
-	cp MacOS-X/ReadMe.rtf.template MacOS-X/Resources/ReadMe.rtf
-	# Builds the pkg file
-	MacOS-X/package $(ARCHINSTALL) MacOS-X/coq-$(VERSION).info -r MacOS-X/Resources
-
-
-macosx-dmg:
-	rm -f $(MACOSXDMG)
-	# We successively :
-	# - create the dmg file
-	# - bind it to a device /dev/diskXs2 (name)
-	# - create the file system and name it "Coq X.X"
-	# - unbind the device and mount the image on /Volumes
-	# - copy the package
-	# - unbind again the image for cleaning up the installation
-	(export size=`du -s $(MACOSXPKG) | cut -dc -f 1`;\
-	hdiutil create -sectors `expr $$size + 1000` $(MACOSXDMG);\
-	export name=`hdid -nomount $(MACOSXDMG) | tail -1 | cut -d" " -f 1`;\
-	newfs_hfs -v "Coq $(VERSION)" $$name;\
-	hdiutil detach $$name;\
-	export name=`hdid $(MACOSXDMG) | tail -1 | cut -d" " -f 1`;\
-	ditto -rsrcFork -v $(MACOSXPKG) "/Volumes/Coq $(VERSION)/$(MACOSXPKG)";\
-	hdiutil detach $$name)
-
-
-###################################################################
-# contribs and patches
-#
-contrib-tag:
-	echo -n "Tagging the contrib with version number $(CVSTAG)...";\
-	cvs rtag -F $(CVSTAG) contrib
-	@echo done
-
-contrib-tar-gz:
-	- rm -rf contrib-$(VERSION)
-	@echo -n Exporting a fresh copy of the contribs...
-	cvs export -d contrib-$(VERSION) -r $(CVSTAG) contrib
-	@echo -n Removing the maintenance files ...
-	@rm -rf contrib-$(VERSION)/*/*/bench.log
-	@rm -rf contrib-$(VERSION)/Lyon/PROGRAMS
-	@find contrib-$(VERSION) -name ".cvsignore" -exec rm {} \;
-	@echo done
-	- rm contrib-$(VERSION).tar.gz
-	@echo -n Building the tar.gz contrib package
-	@tar cvf contrib-$(VERSION).tar contrib-$(VERSION)
-	@gzip --best contrib-$(VERSION).tar
-	@echo done
-
-
-patch: $(COQPACKAGE)
-	scp pauillac.inria.fr:$(FTPDIR)/V$(PREVIOUSVERSION)/coq-$(PREVIOUSVERSION).tar.gz .
-	rm -rf coq-$(PREVIOUSVERSION)
-	gunzip -c coq-$(PREVIOUSVERSION).tar.gz | tar xf -
-	(diff -rc coq-$(PREVIOUSVERSION) $(COQPACKAGE)\
-	 > patch-$(VERSION)-$(PREVIOUSVERSION);\
-	 gzip --best patch-$(VERSION)-$(PREVIOUSVERSION))
-
-###################################################################
-# Installation in the ftp repository
-#
-
-ftp-install: prep-ftp-install
-	$(CP) $(COQPACKAGE)/CHANGES $(FTPVDIR)/
-	$(CP) $(COQPACKAGE)/README $(FTPVDIR)/
-	$(CP) $(COQPACKAGE)/README.win $(FTPVDIR)/
-	$(CP) $(COQPACKAGE)/README.macosx $(FTVPDIR)/
-	$(CP) $(TARGZ) $(FTPVDIR)/
-	$(CP) $(COQPACKAGE)-*.tar.gz $(FTPVDIR)/
-	$(CP) $(COQRPMPACKAGE).*.rpm $(FTPVDIR)/
-
-# prep-ftp-install: $(FTPDIR)/V$(VERSION)
-prep-ftp-install: 
-	- $(SERVEREXEC) mkdir -p -m g+w $(FTPDIR)/V$(VERSION)
-
-final-ftp-install:
-	$(SERVEREXEC) "'(cd $(FTPDIR); rm -f current;ln -sf V$(VERSION) current)'"
-
-tar-gz-ftp-install: prep-ftp-install
-	chmod g+w $(TARGZ)
-	$(CP) $(TARGZ) $(FTPVDIR)/
-
-src-rpm-ftp-install: prep-ftp-install
-	chmod g+w $(COQSRCRPM)
-	$(CP) *.src.rpm $(FTPVDIR)/
-
-arch-rpm-ftp-install: prep-ftp-install
-	chmod g+w $(COQRPM)
-	$(CP) *.$(ARCH).rpm $(FTPVDIR)/
-
-arch-tar-gz-ftp-install: prep-ftp-install
-	chmod g+w $(ARCHTARGZ)
-	$(CP) $(ARCHTARGZ) $(FTPVDIR)/
-
-contrib-ftp-install: prep-ftp-install
-	chmod g+w contrib-$(VERSION).tar.gz
-	$(CP) contrib-$(VERSION).tar.gz $(FTPVDIR)/
-
-patch-ftp-install: prep-ftp-install
-	chmod g+w patch-$(VERSION)-$(PREVIOUSVERSION).gz
-	$(CP) patch-$(VERSION)-$(PREVIOUSVERSION).gz $(FTPVDIR)/
-
-###################################################################
-# Special targets
-#
-
-#clean::
-
-cleanall:: clean
-	rm -f config.distrib
-
diff --git a/distrib/NEWCONTRIB.howto b/distrib/NEWCONTRIB.howto
deleted file mode 100644
index a0466081d5..0000000000
--- a/distrib/NEWCONTRIB.howto
+++ /dev/null
@@ -1,103 +0,0 @@
-       Procédure d'ajout d'une nouvelle contribution Coq
-       -------------------------------------------------
-
-A) INTÉGRATION DE LA CONTRIBUTION À L'ARCHIVE CVS
-
-   Dans l'archive des contributions nouvelle syntaxe ("constr/contrib8",
-   aliasée à "contrib" dans l'archive pauillac:/net/pauillac/constr/ARCHIVE).
-
-1) Si la contribution provient d'une institution qui n'a pas encore
-   contribué, créer un répertoire du nom de l'institution.
-
-2) Dans le répertoire associé à l'institution, créer un répertoire du nom de
-   la contribution. S'assurer que le nom est significatif.
-
-3) Placer la contribution soumise dans ce répertoire et vérifier
-   qu'elle compile avec la version bugfix de la version de Coq
-   actuellement distribuée (ci-dessous appelée version X.XX).
-
-4) S'assurer que les fichiers Make et Makefile existent et sont dans
-   le format standard de coq_makefile, et récursivement dans les
-   sous-répertoires. Sinon, standardiser Make et Makefile et vérifier
-   que cela continue de compiler.
-
-5) Ajouter le nouveau répertoire du Make se trouvant dans le
-   répertoire de l'institution et reconstruire le Makefile associé.
-
-6) Si l'institution est nouvelle, ajouté son nom au Make et au
-   Makefile principal de l'archive contrib (attention, Makefile n'est
-   pas auto-engendré, c'est Makefile.sites qui l'est).
-
-7) Vérifier que l'auteur de la contribution a soumis un fichier
-   description et que les champs sont correctement nommés. Vérifier
-   l'orthographe, etc. S'assurer que le fichier description est à la
-   racine du répertoire associé à la contribution. Vérifier que
-   l'identifiant "Name" (ci-dessous appelé CONTRIBNAME) associé à la
-   contribution est significatif et pas déjà pris par une autre
-   contribution.
-
-8) Si la contribution a un fichier jouant le rôle d'un README,
-   s'assurer qu'il s'appelle bien README quitte à le renommer (par
-   exemple "readme" doit être renommé).
-
-9) Commiter l'ajout du ou des nouveaux répertoires et fichiers, ainsi
-   que la modification des différents Make et Makefile (et éventuellement
-   Makefile.sites).
-
-10) Si la contribution compile bien, on peut déplacer le tag associé à
-   la version actuellement distribuée vers les nouveaux fichiers et
-   répertoires (utiliser "cvs tag -F nom-du-tag noms-des-fichiers").
-
-B) INTÉGRATION À LA SECTION CONTRIBUTIONS UTILISATEURS DU SITE WEB 
-
-   Sur la section contributions du site web de Coq (module www sur
-   pauillac.inria.fr:/net/pauillac/constr/ARCHIVE, sous-répertoire
-   coq/contribs)
-
-1) Déterminer la ou les catégories et sous-catégories dans laquelle
-   classer la nouvelle contribution. Le cas échéant, ajouter une
-   nouvelle sous-catégorie.
-
-2) Dans le ou les fichiers .prehtml associés à cette ou ces
-   catégories, ajouter un item bilingue avec le nom de la
-   contribution, son identifiant, et les auteurs.
-
-3) Faire "make" dans le répertoire www/coq/contribs après avoir
-   configurer ../config avec le tag de la version courante de Coq et
-   s'être assuré que contrib-X.XX était effacé.
-
-   Cette étape nécessite la présence de htmlpp.
-   Attention il y a (au moins) deux programmes qui portent ce nom sur le web. 
-   Ici on a besoin de celui-ci : http://htmlpp.sourceforge.net/
-
-4) Faire une mise à jour partielle du site web de coq:
-
-   export MACHINE=pauillac.inria.fr
-   export WEB=/net/yquem/infosystems/www/logical/coq/contribs
-   export FTP=/net/pauillac/infosystems/ftp/coq/coq/current
-   #
-   # installer les infos des contributions dans le répertoire web coq/contribs
-   #
-   scp all-contribs/CONTRIBNAME.{tar.gz,html,description}\
-     all-contribs/search.db all-contribs/summary.html *.html $MACHINE:$WEB
-   ssh $MACHINE chmod -f g+w $WEB/*
-   #
-   # installer la nouvelle archive de toutes les contribs
-   #
-   scp contrib-X.XX.tar.gz $MACHINE:$FTP
-   ssh $MACHINE chmod -f g+w $FTP/contrib-X.XX.tar.gz
-   #
-   # installer la nouvelle contribution dans le répertoire d'archivage
-   # des contribution par numéro de version de Coq
-   #
-   scp all-contribs/CONTRIBNAME.tar.gz \
-     $MACHINE:/net/yquem/infosystems/www/logical/coq/contributions/VX.XX
-
-5) S'assurer que le site web de coq a été mis à jour correctement, que
-   la nouvelle contribution apparaît dans les versions anglaise et
-   française du classement thématique, ainsi que dans la liste
-   complète. Vérifier que l'outil de recherche par mot-clé la trouve.
-
-6) Commiter les modifications faites à l'archive www/coq/contribs
-
-7) Confirmer à l'auteur l'installation de sa contribution 
diff --git a/distrib/RELEASE b/distrib/RELEASE
deleted file mode 100644
index ef84410f9a..0000000000
--- a/distrib/RELEASE
+++ /dev/null
@@ -1,463 +0,0 @@
-(**************************************************************************)
-(*               Liste des choses à faire pour une release                *)
-(*                          Mise à jour V7                                *)
-(**************************************************************************)
-
-PLAN
-
-A) LE LOGICIEL (SOURCES ET BINAIRES)
-B) LES CONTRIBS
-C) LA DOC
-D) LE SERVEUR WEB
-E) LE CDROM (indépendant de la release)
-
-(**************************************************************************)
-A) LE LOGICIEL
-
-A1) VÉRIFICATIONS
-
-  S'assurer que les choses suivantes été réalisées et COMMITÉES.
-
-  - Changement du magic number dans library/library.ml si la syntaxe
-    interne des .vo a changé
-
-  - Changement des variables en tête du fichier "configure" et
-    vérification du numéro de versions de OCaml et Camlp4 demandées
-  - Mise à jour des champs Version, Source et éventuellement Require 
-    et setup dans RH/coq*.spec
-  - Mise à jour des dépendances dans debian/control. Ajouter une référence
-    à la version et un "* New upstream version" dans debian/changelog.
-    [Note: archive debian maintenant engendrée par Debian eux-mêmes]
-  - Relecture des fichiers "README", "README.win", en particulier,
-    vérification du numéro de version, des adresses internet et des
-    coordonnées de Coq
-  - Relecture des fichiers "INSTALL", "INSTALL.win", "INSTALL.macosx",
-    en particulier numéro de version de coq et numéros des versions de
-    OCaml et Camlp4 demandées
-  - Mise à jour/nettoyage du fichier CHANGES et du fichier ANNONCE
-  - Mise à jour des fichiers .dep.ps dans le répertoire doc (faire make
-    depend depuis ce répertoire)
-
-  S'assurer aussi que make world, make doc et make check fonctionnent !
-
-  EN CAS DE MODIFICATION DE L'ARCHIVE, REPRENDRE EN A3
-  (ou en A2 si la date ou le numéro de version a changé)
-
-  Dans le cas simple d'une recompilation sur une autre architecture,
-sauter A3. Sauter aussi A4 s'il est possible de mettre le fichier
-coq-X.Y.Z.tar.gz à la main dans distrib.
-
-A2) CONFIGURATION DES PARAMETRES DE LA DISTRIBUTION
-
-  Se placer dans le répertoire distrib et faire
-
-     ./configure.distrib
-
-  pour positionner les paramètres de la distrib (les paramètres par
-défaut sont obtenus via le fichier "../configure". Si celui-ci n'est
-pas conforme à l'archive (sans doute peu probable, mais cela m'est
-arrivé), il faut donner les valeurs à la main.
-
-A3) ESTAMPILLAGE DE L'ARCHIVE
-
-  Toujours dans le répertoire distrib, faire
-
-     make tag
-
-  pour poser le tag V'X'-Y-Z à l'archive V'X' (on suppose que le numéro
-  de version donné dans configure.distrib est V'X'.Y.Z).
-
-  Si le tag est à poser sur une branche, il ne faut pas utiliser "make tag"
-mais faire à la main
-
-  cvs rtag -r branch-tag VX-Y-Z 
-
-  La commande "make tag" peut être refaite plusieurs fois auquel cas
-l'ancienne marque est supprimée avant d'être remise à la nouvelle
-place.
-
-  Pour ne modifier qu'un fichier isolément sans retagger toute
-l'archive faire "cvs tag -F V6-2-5 nom_du_fichier".
-
-
-A4) CREATION DU PACKAGE SOURCE
-
-  Créer le coq-X.Y.Z.tar.gz des sources à partir d'un extrait tout
-frais (obtenu par cvs export) de l'archive avec
-
-     make tar-gz
-
-  En particulier, les fichiers à ne pas distribuer (dont le répertoire
-distrib, le TODO, etc) sont retirés (rebrancher aussi dans le Makefile
-le répertoire theories/Num quand il sera opérationnel). Cette commande
-fait dérouler une check-list. Si on l'interrompt ou qu'elle échoue, le
-tar-gz reste créé et c'est à la charge de l'utilisateur de s'assurer
-que les paramètres sont corrects.
-
-  Pour l'installation sous ftp voir A7.
-
-A5) CREATION DES PACKAGES BINAIRES (ad libitum)
-   (prévoir pour chaque package près de 100Mo dispo sur la partition)
-
-A5a) Création d'un package binaire tar.gz 
-
-      make arch-tar-gz
-
-  dans le répertoire distrib sous l'architecture ARCH avec le système SYS
-crée un fichier coq-X.Y.Z-SYS-ARCH.tar.gz (ex : coq-6.2.5-alpha-OSF1.tar.gz).
-
-  Pour compiler sur plusieurs machines en parallèle, il faut des
-répertoires "distrib" distincts pour que les compilations ne se
-téléscopent pas. Sur une 2ème machine dans un autre répertoire
-"distrib", refaire "make tar-gz" en interrompant la check-list (ou
-simplement copier le coq-X.Y.Z.tar.gz déjà fait) puis "make arch-tar-gz".
-
-  Pour l'installation sous ftp voir A7.
-
-  Remarque : ce binaire est prévu pour être dé-tar-ré dans / avec une
-installation dans /usr/local/bin.
-
-A5b) Création des sources rpm et des premiers packages rpm
-
-     make rpm
-
-  dans le répertoire distrib sous l'architecture ARCH crée un package
-source coq-X.Y.Z-1.src.rpm et un package binaire coq-X.Y.Z-1.ARCH.rpm
-(ex : coq-6.2.5-1.i386.rpm).
-
-  Remarques : 1) Les packages Intel s'appellent i386 même si
-l'architecture est i586 ou i686 (faux avec rpm 3.0). 2) Les rpm sont
-prévus pour une installation dans /usr/bin (!).
-
-  Pour l'installation sous ftp voir A7.
-
-A5c) Création d'un second package rpm à partir des sources rpm
-
-  Faire 
-
-     make arch-rpm
-
-  sous une autre architecture pour créer un deuxième package rpm binaire.
-
-  Pour l'installation sous ftp voir A7.
-
-A5d) Création d'un package coq-ide (normalement fait par "make rpm")
-
-  Faire un
-
-     make rpm-ide
-
-  pour produire un package source coqide-X-Y-Z-1.src.rpm et un package
-  bianire coqide-X-Y-Z-1.ARCH.rpm.
-
-A5e) Création du package debian
-
-  Faire un
-
-     make deb
-
-  pour faire paquets source et binaire sur une machine debian
-  (pc8-118.lri.fr par exemple). Pas la peine d'essayer de créer le
-  binaire sur toutes les architectures : ce sera fait par les machines
-  de Debian dès que le paquet source leur sera fourni.
-
-A5f) Création du package windows
-
-  Habituellement fait sur jurancon.inria.fr, sous Windows NT, avec la
-  version Win32 de ocaml (pas la version cygwin car elle produit un
-  coqtop exécutable que sous cygwin) installée dans un répertoire ne
-  contenant pas d'espace, avec les variables CAMLLIB et CAMLP4LIB
-  positionnée (ainsi que ocamlc et camlp4 dans le PATH).
-
-  Faire un
-
-     make win
-
-  pour créer une archive zip.
-
-  Envoyer ensuite l'archive par ftp dans
-
-    pauillac:/net/pauillac/infosystems/ftp/coq/coq/V'X'.Y.Z
-
-A6) CREATION DU FICHIER DE PATCH (attention ne marche pas sur DEC je crois)
-
-    make patch (pas déboggué)
-
-  Pour créer un fichier de patch entre la version à distribuer et la
-version précédente se trouvant dans l'archive (supposée être la même
-que celle taggée V6-2-4 (version -1) dans l'archive CVS...).
-
-Remarque: On peut faire un patch aussi par
-
-  cvs rdiff -r V6-2-4 -r V6-2-5 V6-2 > patch-coq-6.2.4-6.2.5
-
-  Mais il faut alors éditer pour supprimer les références aux
-répertoires distrib et doc, aux fichiers TODO, KNOWNBUGS, ANNONCE et
-les .cvsignore .
-
-
-A7) INSTALLATION SOUS FTP
-
-   make ftp-install # Avec les droits du groupe coq
-
-   - crée le dossier /net/pauillac/infosystems/ftp/coq/coq/V'X'.Y.Z, le
-   lie symboliquement à /net/pauillac/infosystems/ftp/coq/coq/current.
-
-   - installe sous ftp tous les fichiers tar.gz ou .rpm du répertoire
-  distrib (sources et binaires), ainsi que le fichier CHANGES
-
-  Pour installer seulement un des packages, faire au choix
-
-    make tar-gz-ftp-install
-    make src-rpm-ftp-install
-    make arch-rpm-ftp-install
-    make arch-tar-gz-ftp-install
-
-  À faire : ne mettre le lien current qu'au dernier moment.
-
-A8) VÉRIFICATION GÉNÉRALE
-
-  Télécharger et utiliser 24 heures la version FTP
-
-    # sur SunOS, Next, ...
-    ncftp ftp://ftp.inria.fr/INRIA/coq/V6.2.5/V6.2.5.tar.gz
-    tar xvzf V6.2.5.tar.gz
-    cd V6.2.5
-    yes "" | ./configure
-    make world-opt world
-    make cleanall world world-opt
-    make install	
-
-    # sur i586
-    ncftp ftp://ftp.inria.fr/INRIA/coq/V6.2.5/coq-6.2.5-1.i586.rpm
-    rpm -Uvh coq-6.2.5-1.i586.rpm
-    coqtop      # etc...
-    coqtop -opt # etc...
-
-    # sur linux ppc et apx
-    ncftp ftp://ftp.inria.fr/INRIA/coq/V6.2.5/coq-6.2.5-1.src.rpm 
-    rpm --recompile coq-6.2.5-1.src.rpm
-    coqtop      # etc...
-    coqtop -opt # etc...
-
-  Cliquer un peu partout sur le serveur coq.inria.fr (rubrique coq
-proof assistant).
-
-  Si jamais quelque chose ne va pas, reprendre à l'étape A2 en retaggant
-l'archive après les modifications (le tag est automatiquement déplacé)
-
-A9) DIFFUSION
-
-  Préparer les contribs (B), la doc (C), le serveur web (D)
-
-  Positionner le lien current du répertoire FTP vers le répertoire de
-  la version ftp à distribuer avec
-
-    make final-ftp-install
-
-  Ouf, c'est prêt... faire l'annonce sur coq-club
-
-
-(**************************************************************************)
-B) LES CONTRIBS
-
-B1) PRÉPARATION 
-
-  Cette phase de vérification est actuellement remplacée par le test
-nocturne coqbench de J.-C. qui permet de savoir ce qui ne passe pas et
-pourquoi.
-
-  Ancienne méthode de vérification :
-
-  - se placer dans une version à jour des contribs (si pas déjà fait,
-le faire avec un "cvs checkout contrib" quelque part en dehors de
-l'archive V6).
-
-  - positionner les variables COQTOP et COQBIN (avec un / à la fin !!)
-sur une version à jour de l'archive V6 et s'assurer que make opt et
-make passent.
-
-B2) POSE DU TAG
-
-  Dans le répertoire distrib, faire
-
-    make contrib-tag
-
-  pour poser le tag V6-2-5
-  (ceci est équivalent à "cvs rtag -F V6-2-5 contrib")
-
-B4) SUPPRESSION DES FICHIERS INUTILES ET CRÉATION DU PACKAGE
-
-  Dans le répertoire distrib, faire
-
-    make contrib-tar-gz
-
-  pour créer contrib-6.2.5.tar.gz
-
-  Attention, le répertoire PROGRAMS est actuellement retiré (le
-réactiver dans le Makefile si besoin est). Les fichiers bench.log
-sont aussi retirés.
-
-
-B5) INSTALLATION SOUS FTP
-
-  Dans le répertoire distrib, faire
-
-    make contrib-ftp-install
-
-  pour installer le package contrib-6.2.5.tar.gz en ftp
-
-
-(**************************************************************************)
-C) LA DOC
-
-  La doc se prépare à partir du répertoire cvs "doc". Sa compilation
-nécessite la présence dans le path d'une archive Coq correspondant au
-tag de la release.
-
-C1) PRÉPARATION
-
-  S'assurer que les outils suivants sont disponibles
-
-    Dvi: latex (latex2e), bibtex, makeindex, dviselect (rpm dviutils)
-    Ps: dvips, psselect (package psutils)
-    Pdf: pdflatex (optionnel)
-    Html: hevea (par Luc Maranget), htmlsplit (plus utilisé depuis Coq 8.0)
-
-  Mettre à jour les fichiers suivants :
-
-  - Tutorial.tex : numéro de version et date (1 fois)
-  - title.tex    : numéro de version
-  - cover.html   : numéro de version (2 fois)  et date
-  - README       : numéros de version (2 fois)
-  - Makefile     : numero de version
-
-  Vérification que "CHANGES" est à jour par rapport à "Changes.tex"
-(obsolète, plus de Changes.ps mais un Changes.html engendré
-manuellement à partir de CHANGES).
-
-  Faire un make clean; grep V6 *.{tex,sty,html} pour s'assurer
-qu'aucun autre V6.? ne traine.
-
-  Les fichiers Tutorial-cover.tex et RefMan-cover.tex ne servent que
-pour faire des rapports INRIA.
-
-  Si un fichier Anomaly.dvi doit être distribué, s'en occuper à la main
-(ou modifier le Makefile en conséquence).
-
-  Si un fichier Changes.dvi doit être distribué, s'en occuper à la main
-(ou modifier le Makefile en conséquence).
-
-C2) ESTAMPILLAGE
-
-  Faire 
-
-  cvs rtag -F V7-1 doc
-
-  pour tagger l'archive avec le numéro de la version de Coq auquel
-  elle correspond
-
-C3) COMPILATION
-
-  Pour compiler l'ensemble des fichiers de documentation à installer
-sous ftp et/ou sur le serveur web, faire dans le répertoire doc
-
-    make distrib
-
-  qui crée les versions dvi.gz, ps.gz, pdf.gz de la doc, les packages
-all-ps-doc.tars.gz et doc-html.tar.gz ainsi qu'un répertoire www
-recopiable sur le site web
-
-  Si la doc est modifiée après le tagguage des sources Coq, retagguer
-la doc séparemment depuis le répertoire doc avec
-
-  cvs tag -F V6-2-5 * library/*
-
-C4) LA BIBLIO STANDARD AU FORMAT COQDOC
-
-  Le package library-X.Y.tar.gz sa fait dans l'archive cvs du site
-web, répertoire www/coq/library. Il faut au préalable mettre à jour le
-fichier www/coq/config avec le bon tag de version. La cible est alors
-
-    make pages
-
-  Elle exporte une archive fraiche correspondant au tag du fichier
-config, puis recompile la bibliothèque standard en exportant les
-références globales. Elle applique ensuite coqdoc à la bibliothèque
-standard puis crée un paquet des pages html obtenues.
-
-  Il faut ensuite installer ce paquet à la main sur le site ftp.
-
-C5) INSTALLATION SOUS FTP
-
-    Après avoir positionner la variable VERSION à V6.2.5, installer
-la doc sous ftp depuis le répertoire doc avec
-
-    make doc-ftp-install
-
-    On retrouve alors sous ftp avec le README, plusieurs couples
-    .dvi.gz et .ps.gz, le tar de la doc html, le tar des docs en ps.
-
-    Ajouter à la main le fichier CHANGES de l'archive Coq dans 
-    
-      /net/pauillac/infosystems/ftp/coq/coq/V6.2.5/doc
-
-(**************************************************************************)
-D) LE SERVEUR WEB
-
-D1) PRÉPARATION
-
-   Cela se fait sous CVS : faire un check-out ou update du module
-"www" quelque part chez soi en dehors de l'archive V6
-
-   - se placer dans le sous-répertoire "coq" de l'archive "www"
-
-   - mettre à jour les fichiers suivants du répertoire coq (numéro de
-     version, version nécessaires de ocaml et camlp4, date de mise à
-     jour)
-
-     distrib1-fra.html et distrib1-eng.html,
-     contribs1-fra.html et contribs1-eng.html (dont un ajout de ligne à la fin)
-     coq1-eng.html et coq1-fra.html
-     doc1-eng.html et doc1-fra.html
-
-   - commiter
-
-   - créer un fichier Changes.html à partir du fichier CHANGES et le
-     déposer dans /net/pauillac/infosystems/ft/coq/V6.2.5/doc (ce
-     fichier est pointé par les pages coq1-fra.html et coq1-eng.html)
-
-   - à partir de sa copie locale du répertoire www, faire
-  
-     (cd coq/contribs; make pages)
-
-   - positionner la variable THEORIES sur le repertoire theories
-     d'une copie fraîche de l'archive et faire (sur PAUILLAC et avec
-     gmake parce qu'un binaire devant tourner sur pauillac est fabriqué)
-
-     (cd coq/library; gmake pages)
-
-D2) ACTUALISATION DU SERVEUR WEB
-
-     Enfin, faites-en part au monde entier :
-
-     make install-coq
-     (cd coq/contribs; make install)
-     (cd coq/library; make install)
-
-
-(**************************************************************************)
-E) LE CDROM
-
-  Tout est en place dans /net/pauillac/constr/cdrom. S'y rendre et 
-
-  - mettre à jour les fichiers prog/{unix,pc,mac}/coq/{fra,eng}.htm
-  - mettre à jour les liens dans ftp/coq 
-	(1 lien pour la version Mac, 1 lien pour les autres architectures).
-  - vérifier que projs/logical/{fra,eng}.htm et *.html sont corrects
-
-Pour les sites www (coq et logical) faire une copie et modifier les
-liens relatifs suivant l'architecture du cdrom.
-
-
-
diff --git a/distrib/RH/coq.spec b/distrib/RH/coq.spec
deleted file mode 100644
index 30a1e577dd..0000000000
--- a/distrib/RH/coq.spec
+++ /dev/null
@@ -1,52 +0,0 @@
-Name: coq
-Version: 8.0
-Release: 2
-Summary: The Coq Proof Assistant
-Copyright: freely redistributable
-Group: Applications/Math
-Vendor: INRIA & LRI
-URL: http://coq.inria.fr
-Source: ftp://ftp.inria.fr/INRIA/coq/V8.0/coq-8.0.tar.gz
-Icon: petit-coq.gif
-BuildRoot: /var/tmp/coq
-
-%description
-Coq is a proof assistant which: 
-  - allows to handle calculus assertions, 
-  - check mechanically proofs of these assertions, 
-  - helps to find formal proofs, 
-  - extracts a certified program from the constructive proof
-    of its formal specification, 
-
-Requires: ocaml >= 3.06
-
-%define debug_package %{nil}
-                                                                               
-%prep
-%setup
-
-%build
-./configure -bindir %{_bindir} -libdir %{_libdir}/coq -mandir %{_mandir} \
-   -emacslib %{_datadir}/emacs/site-lisp \
-   -coqdocdir %{_datadir}/texmf/tex/latex/misc \
-   -opt -reals all -coqide no
-make coq
-
-
-%clean
-rm -rf %{buildroot}
-make clean
-
-%install
-rm -rf %{buildroot}
-make -e COQINSTALLPREFIX=%{buildroot} install-coq
-
-%define __spec_install_post /usr/lib/rpm/brp-compress
-
-%files
-%defattr(-,root,root)
-%{_bindir}/*
-%{_libdir}/coq
-%{_mandir}/man1/*
-%{_datadir}/emacs/site-lisp/*
-%{_datadir}/texmf/tex/latex/misc/*
diff --git a/distrib/RH/coq_ext_for_pcoq.spec b/distrib/RH/coq_ext_for_pcoq.spec
deleted file mode 100644
index 954be7239d..0000000000
--- a/distrib/RH/coq_ext_for_pcoq.spec
+++ /dev/null
@@ -1,45 +0,0 @@
-Name: coq_ext_for_pcoq
-Version: 8.0
-Release: 2
-Summary: The Coq Extension for Pcoq
-Copyright: freely redistributable
-Group: Applications/Math
-Vendor: INRIA & LRI
-URL: http://coq.inria.fr
-Source: ftp://ftp.inria.fr/INRIA/coq/V8.0/coq-8.0.tar.gz
-Icon: petit-coq.gif
-Requires: coq = 8.0
-BuildRoot: /var/tmp/pcoq
-
-%description
-The Coq Extension for Pcoq provides all facilities to interface Coq with
-Pcoq
-
-%define debug_package %{nil}
-
-%prep
-%setup -n coq-8.0
-
-%build
-./configure -bindir %{_bindir} -libdir %{_libdir}/coq -mandir %{_mandir} \
-   -emacslib %{_datadir}/emacs/site-lisp \
-   -coqdocdir %{_datadir}/texmf/tex/latex/misc \
-   -opt -reals all -coqide no
-make pcoq
-
-%clean
-rm -rf %{buildroot}
-make clean
-
-%install
-rm -rf %{buildroot}
-make -e COQINSTALLPREFIX=%{buildroot} install-pcoq
-
-%define __spec_install_post /usr/lib/rpm/brp-compress
-
-%files
-%defattr(-,root,root)
-%{_bindir}/*
-%{_libdir}/coq/contrib/interface
-%{_mandir}/man1/*
-
diff --git a/distrib/RH/coqide.spec b/distrib/RH/coqide.spec
deleted file mode 100644
index 3fd25c4231..0000000000
--- a/distrib/RH/coqide.spec
+++ /dev/null
@@ -1,56 +0,0 @@
-Name: coqide
-Version: 8.0
-Release: 2
-Summary: The Coq Integrated Development Interface
-Copyright: freely redistributable
-Group: Applications/Math
-Vendor: INRIA & LRI
-URL: http://coq.inria.fr
-Source: ftp://ftp.inria.fr/INRIA/coq/V8.0/coq-8.0.tar.gz
-Icon: petit-coq.gif
-Requires: coq = 8.0
-BuildRoot: /var/tmp/coqide
-
-%description
-The Coq Integrated Development Interface is a graphical interface for the 
-Coq proof assistant 
-
-%define debug_package %{nil}
-
-%prep
-%setup -n coq-8.0
-
-%build
-./configure -bindir %{_bindir} -libdir %{_libdir}/coq -mandir %{_mandir} \
-   -emacslib %{_datadir}/emacs/site-lisp \
-   -coqdocdir %{_datadir}/texmf/tex/latex/misc -opt -reals all
-make coqide
-
-%clean
-rm -rf %{buildroot}
-make clean
-
-%install
-rm -rf %{buildroot}
-make -e COQINSTALLPREFIX=%{buildroot} install-coqide
-
-# menu entry
-mkdir -p %{buildroot}%{_menudir}
-cat > %{buildroot}%{_menudir}/CoqIDE << _EOF_
-?package(CoqIDE): \
- command="%{_bindir}/coqide" \
-# icon="coqide.png" \ TODO add an icon
- longtitle="The Coq Integrated Development Interface" \
- needs="x11" \
- section="Applications/Sciences/Mathematics" \
- title="CoqIDE" \
- startup_notify="yes"
-_EOF_
-
-%define __spec_install_post /usr/lib/rpm/brp-compress
-
-%files
-%defattr(-,root,root)
-%{_menudir}/CoqIDE
-%{_bindir}/*
-%{_libdir}/coq/ide
diff --git a/distrib/RH/do_build b/distrib/RH/do_build
deleted file mode 100644
index 103d4a880a..0000000000
--- a/distrib/RH/do_build
+++ /dev/null
@@ -1,2 +0,0 @@
-./configure -prefix /usr -emacslib /usr/share/emacs/site-lisp -opt -reals all -coqide no       # Need ocamlc.opt and ocamlopt.opt
-make coq       # Use native coq to compile theories
diff --git a/distrib/RH/do_build_pcoq b/distrib/RH/do_build_pcoq
deleted file mode 100755
index 0477d001bd..0000000000
--- a/distrib/RH/do_build_pcoq
+++ /dev/null
@@ -1,2 +0,0 @@
-./configure -prefix /usr -emacslib /usr/share/emacs/site-lisp -opt -reals all -coqide no       # Need ocamlc.opt and ocamlopt.opt
-make pcoq      # Use native coq to compile theories
diff --git a/distrib/check-list b/distrib/check-list
deleted file mode 100755
index c0e547062a..0000000000
--- a/distrib/check-list
+++ /dev/null
@@ -1,90 +0,0 @@
-#!/bin/sh
-
-. ./config.distrib
-
-echo
-echo The Coq Check List
-echo ------------------
-echo
-
-COQPACKAGE=coq-$VERSION
-CONFIGFILE=$COQPACKAGE/configure
-
-version=`grep "^VERSION=" $CONFIGFILE | sed -e 's/^VERSION=\(.*\)/\1/'`
-coqdate=`grep "^DATE=" $CONFIGFILE | sed -e 's/^DATE=\(.*\)/\1/'`
-
-echo "According to the configure file of the archive to be released"
-echo "  The release version is V$version"
-echo "  The date is $coqdate"
-echo
-echo "Comparing datas with expected ones"
-
-if [ ! "$version" = "$VERSION" ]; then
-	 echo "Inconsistent version number";exit
-fi
-if [ ! "$date" = "$DATE" ]; then
-	echo "Inconsistent date release";exit
-fi
-
-echo "Please answer y or n to questions"
-
-if grep $version $COQPACKAGE/library/library.ml > /dev/null; then
-  echo "Found a reference to $version in library.ml..."
-  echo "   ... I guess the magic numbers have been changed"
-else
-  echo 'Found no trace that the magic numbers are changed in library.ml'
-  echo -n 'Is it still OK? '
-  read a
-  if [ "$a" != 'y' -a "$a" != 'Y' ]; then echo Aborting; exit 1; fi
-fi
-
-readmeversion=`grep "THE COQ .* SYSTEM" $COQPACKAGE/README | sed -e 's/.*THE COQ \(.*\) SYSTEM.*/\1/'`
-if [ "$readmeversion" = "" ]
-then echo "Failed to find version number in README; please check by hand"
-else
-  echo -n The README file seems to mention version number $readmeversion ...
-  if [ $readmeversion = V$version ]
-  then echo " it seems OK"
-  else echo -n " is that really OK? "
-     read a
-     if [ "$a" != 'y' -a "$a" != 'Y' ]; then echo Aborting; exit 1; fi
-  fi
-fi
-
-readmewinversion=`grep "THE COQ .* SYSTEM" $COQPACKAGE/README.win | sed -e 's/.*THE COQ \(.*\) SYSTEM.*/\1/'`
-if [ "$readmewinversion" = "" ]
-then echo "Failed to find version number in README.win; please check by hand"
-else
-  echo -n The README.win file seems to mention version number $readmewinversion ...
-  if [ $readmewinversion = V$version ]
-  then echo " it seems OK"
-  else echo -n " is that really OK? "
-     read a
-     if [ "$a" != 'y' -a "$a" != 'Y' ]; then echo Aborting; exit 1; fi
-  fi
-fi
-
-ocamlversion=`grep "You need Objective-Caml .* or later" $CONFIGFILE | sed -e 's/.*Objective-Caml \(.*\) or later.*/\1/'`
-echo -n The configure file seems to require O\'Caml version $ocamlversion ...
-echo -n " is that OK? "
-read a
-if [ "$a" != 'y' -a "$a" != 'Y' ]; then echo Aborting; exit 1; fi
-
-versionspec1=`sed -n -e 's!^Version: \(.*\)!\1!p' ./RH/coq.spec`
-versionspec2=`sed -n -e 's!^Source: .*coq-\(.*\)\.tar\.gz.*!\1!p' ./RH/coq.spec`
-if [ "$versionspec1" = "$version" -a "$versionspec2" = "$version" ];
-then echo "Version number in coq.spec seems OK ($versionspec1)";
-else
-  echo "Wrong version numbers in coq.spec ($versionspec1 and $versionspec2 instead of $version)"
-  echo -n " is that OK? "
-  read a
-  if [ "$a" != 'y' -a "$a" != 'Y' ]; then echo Aborting; exit 1; fi
-fi
-
-#  ocamlversionspec=`grep "^Requires: ocaml" ./coq.spec | sed -e 's/Requires: ocaml >= \(.*\)/\1/'`
-#  if [ "$ocamlversionspec" = "$ocamlversion" ]
-#  then echo "Required version of Objective Caml in coq.spec seems OK ($ocamlversionspec)"
-#  else
-#    echo "Wrong version of required Objective Caml in coq.spec ($ocamlversionspec)"
-#    echo Aborting; exit 1
-#  fi
diff --git a/distrib/configure.distrib b/distrib/configure.distrib
deleted file mode 100755
index 345148ff79..0000000000
--- a/distrib/configure.distrib
+++ /dev/null
@@ -1,95 +0,0 @@
-#!/bin/sh
-
-####################################
-#
-#  Configuration script for releases
-# 
-####################################
-#
-#  Default values comes from ../configure which is probably consistent
-#  with the archive
-#
-
-VERSION=`sed -n -e 's/^VERSION=\(.*\)/\1/p' ../configure`
-DATE=`sed -n -e 's/^DATE=\(.*\)/\1/p' ../configure`
-RELEASENUM=1
-DISTRIBDIR=`pwd`
-
-# i.86 standardized to i386
-# MacOS X returns "Power Macintosh" - changed to "MacOS-X"
-ARCH=`uname -m | sed -e 's/i.86/i386/' -e 's/Power Macintosh/MacOS-X/'`
-
-echo Default values are taken from ../configure
-echo ------------------------------------------
-
-# Determine the release number
-echo -n "Version number of the current release [$VERSION]? "
-read ANSWER
-case $ANSWER in
- "") true;;
- *) VERSION=$ANSWER;
-esac
-
-# The main number of the release
-MAINNUMBER=`echo $VERSION | sed -e 's/^\([0-9][0-9]*\)\.[0-9][0-9]*.*$/\1/'`
-# The minor number
-LASTNUMBER=`echo $VERSION | sed -e 's/^[0-9][0-9]*\.\([0-9][0-9]*\).*$/\1/'`
-# The release level: alpha, beta, etc.
-LEVEL=`echo $VERSION | sed -e 's/^[0-9][0-9]*\.[0-9][0-9]*\(.*\)$/\1/'`
-
-MAJORVERSION=V$MAINNUMBER
-CVSMODULE=V7
-CVSTAG=V`echo $VERSION | sed -e 's/\./-/g'`
-if [ "$LASTNUMBER" = "0" ]; then
-    PREVIOUSMAINNUMBER=`expr $MAINNUMBER - 1`
-    PREVIOUSVERSION=$PREVIOUSMAINNUMBER.99
-else
-    PREVIOUSLASTNUMBER=`expr $LASTNUMBER - 1`
-    PREVIOUSVERSION=$MAINNUMBER.$PREVIOUSLASTNUMBER
-fi
-
-# Determine the previous release number
-echo -n "Version number of the previous release (for the patch file) [$PREVIOUSVERSION]? "
-read ANSWER
-case $ANSWER in
- "") true;;
- *) PREVIOUSVERSION=$ANSWER;;
-esac
-
-
-# Determine the searchisos version number
-#echo -n "What is the version number of the current SearchIsos release [$VERSIONSI]? "
-#read ANSWER
-#case $ANSWER in
-# "") true;;
-# *) VERSIONSI=$ANSWER;;
-#esac
-
-# Determine the date of the release
-echo -n "Date of the current release [$DATE]? "
-read ANSWER
-case $ANSWER in
- "") true;;
- *) DATE=$ANSWER;;
-esac
-
-# Determine the rpm release number
-echo -n "Release number for the RPM packages [$RELEASENUM]? "
-read ANSWER
-case $ANSWER in
- "") true;;
- *) RELEASENUM=$ANSWER;;
-esac
-
-echo CVSMODULE=$CVSMODULE > config.distrib
-echo CVSTAG=$CVSTAG >> config.distrib
-echo DISTRIBDIR=$DISTRIBDIR >> config.distrib
-echo VERSION=$VERSION >> config.distrib
-echo RELEASENUM=$RELEASENUM >> config.distrib
-echo ARCH=$ARCH >> config.distrib
-echo PREVIOUSVERSION=$PREVIOUSVERSION >> config.distrib
-#echo VERSIONSI=$VERSIONSI >> config.distrib
-chmod +x config.distrib
-
-# $Id$
-
diff --git a/distrib/debian/README.Debian b/distrib/debian/README.Debian
deleted file mode 100644
index bb65ad1979..0000000000
--- a/distrib/debian/README.Debian
+++ /dev/null
@@ -1,27 +0,0 @@
-Coq package for Debian
-----------------------
-
-Note that all bytecode files in this package need to be left
-'unstripped' after compiling. The reason is the following:
-
-  It is possible to strip the .out corresponding to ocaml code compiled in
-  native code (and it is done in Coq (coqopt.out) When compiling in
-  byte-code, the Coq system uses the -custom option in order to get an
-  autonomous executable (running independently of an ocaml implementation on
-  your computer). The way it works is that the .out file is composed of the
-  executable of the byte-code interpreter plus the byte-code for your own
-  program which is stored in the symbol table zone...  stripping such an
-  executable, just remove your byte-code and consequentely cannot run
-  properly.
-
-Moreover the bytecode version is installed even on platforms having a
-native version as the dynamic loading of tactics works only with the
-bytecode version.
-
-For interactive use of coqtop, we suggest
-- either the Debian cle package
-- or the Proof-General (x)emacs mode, provided in the proofgeneral-coq
-  Debian package.
-
-
-
diff --git a/distrib/debian/changelog b/distrib/debian/changelog
deleted file mode 100644
index 727d5264c4..0000000000
--- a/distrib/debian/changelog
+++ /dev/null
@@ -1,132 +0,0 @@
-coq (7.4-1) unstable; urgency=low
-
-  * New upstream version.
-  * Should now build native on ppc (ocaml bug being fixed)
-
- -- Judicael Courant <Judicael.Courant@lri.fr>  Wed, 25 Jun 2003 09:49:06 +0200
-
-coq (7.3.1-1) unstable; urgency=low
-
-  * New bugfix upstream version.
-  * Proof General is now Recommended since he has been freed (closes:
-    Bug#162894).
-
- -- Judicael Courant <Judicael.Courant@lri.fr>  Mon,  7 Oct 2002 12:34:03 +0200
-
-coq (7.3-1) unstable; urgency=low
-
-  * New upstream version.
- 
- -- Judicael Courant <Judicael.Courant@lri.fr>  Wed, 22 May 2002 14:48:21 +0200
-
-coq (7.2-9) unstable; urgency=low
-  * ocamlc.opt completely broken on powerpc. Added a special case in
-    "rules" for using only bytecode.
-
- -- Judicael Courant <Judicael.Courant@lri.fr>  Fri, 15 Feb 2002 09:17:20 +0100
-
-coq (7.2-8) unstable; urgency=low
-
-  * "timeout" time is now 5300s (< 90 min).
-
- -- Judicael Courant <Judicael.Courant@lri.fr>  Thu, 14 Feb 2002 17:38:06 +0100
-
-coq (7.2-7) unstable; urgency=low
-
-  * Build now uses ocamlc.opt and ocamlopt.opt if available.
-  * Dependency forced on ocaml >= 3.04 (dependency ocaml >=3.04 | camlp4
-    does not make buildd happy. See http://buildd.debian.org/fetch.php?
-    &pkg=coq&ver=7.2-5&arch=arm&stamp=1013388706&file=log&as=raw).
-
- -- Judicael Courant <Judicael.Courant@lri.fr>  Tue, 12 Feb 2002 09:10:01 +0100
-
-coq (7.2-6) unstable; urgency=low
-
-  * Typo in rules, which made the build process always build in
-    bytecode. Fixed.
-
- -- Judicael Courant <Judicael.Courant@lri.fr>  Mon, 11 Feb 2002 11:22:21 +0100
-
-coq (7.2-5) unstable; urgency=low
-
-  * Pb with timeout, used in 7.2-4 (bug 132927) making the build process
-    fail when compilation in native mode fails. Workaround in rules: after
-    a "timeout ... make ..." we try a "make -q" to check that everything
-    has been done correctly.
-
- -- Judicael Courant <Judicael.Courant@lri.fr>  Fri,  8 Feb 2002 10:08:10 +0100
-
-coq (7.2-4) unstable; urgency=low
-  * Native code compilation failed on sparc; coqtop built by ocamlopt
-    entered an infinite loop on powerpc. Fixed (using timeout for powerpc:
-    if coqtop loops, it is rebuild using the bytecode compiler)
-
- -- Judicael Courant <Judicael.Courant@lri.fr>  Fri,  1 Feb 2002 11:04:25 +0100
-
-coq (7.2-3) unstable; urgency=low
-  * Workaround for problems with buildd/apt trying to install camlp4
-    (closes: Bug#130046).
-  
- -- Judicaël Courant <Judicael.Courant@lri.fr>  Mon, 21 Jan 2002 09:46:16 +0100
-
-coq (7.2-2) unstable; urgency=low
-
-  * Build-Depends now requires camlp4 instead of camlp4 (>=3.01) since
-    camlp4 is a virtual package provided by ocaml >=3.04.
-
- -- Judicaël Courant <Judicael.Courant@lri.fr>  Fri, 11 Jan 2002 11:08:03 +0100
-
-coq (7.2-1) unstable; urgency=low
-  * New upstream version.
-
- -- Judicaël Courant <Judicael.Courant@lri.fr>  Wed,  9 Jan 2002 14:02:42 +0100
-
-coq (7.1-2) unstable; urgency=low
-
-  * Fixed policy problem (conf files).
-  * Trying to compile in bytecode if native code compilation fails
-    (closes: Bug#119714)
-  * Errors raised by the Simpl tactic is an upstream bug and should
-    have been fixed in 7.0 (closes: Bug#74518).
-
- -- Judicaël Courant <Judicael.Courant@lri.fr>  Tue, 11 Dec 2001 13:33:15 +0100
-
-coq (7.1-1) unstable; urgency=low
-  * New upstream version.
-
- -- Judicaël Courant <Judicael.Courant@lri.fr>  Tue,  25 Sep 2001 16:27:04 +0200
-
-coq (7.0-1) unstable; urgency=low
-  * New maintainer Judicaël Courant <Judicael.Courant@lri.fr>.
-  * New upstream version.
-  * Added Build-Depends (closes: Bug#70273).
-  * Cleaned up dependencies.
-  * Emacs mode installation now follows Emacs policy.
-  * Made compilation non-interactive (closes: Bug#92461).
-  * Added Suggests cle.
-  
-
- -- Judicaël Courant <Judicael.Courant@lri.fr>  Tue,  17 Apr 2001 19:24:34 +0200
-
-coq (6.3.1-3) unstable; urgency=low
-
-  * Patched to allow use of ocaml3.
-
- -- Fernando Sanchez <fer@debian.org>  Fri,  7 Jul 2000 08:05:47 +0200
-
-coq (6.3.1-2) unstable; urgency=low
-
-  * Some changes to allow successful porting of this package:
-  * Added checking for ocamlopt.opt before running ./configure with -opt,
-    and configure without it if it is not present for this architecture.
-  * Added checking for ocamlopt before making world-opt.
-
- -- Fernando Sanchez <fer@debian.org>  Sat, 18 Dec 1999 16:45:01 +0100
-
-coq (6.3.1-1) unstable; urgency=low
-
-  * Initial Release.
-
- -- Fernando Sanchez <fer@debian.org>  Fri,  3 Dec 1999 22:06:04 +0100
-
-
diff --git a/distrib/debian/control b/distrib/debian/control
deleted file mode 100644
index cb5c43578f..0000000000
--- a/distrib/debian/control
+++ /dev/null
@@ -1,18 +0,0 @@
-Source: coq
-Section: devel
-Priority: optional
-Maintainer: Judicaël Courant <Judicael.Courant@lri.fr>
-Standards-Version: 3.5.3
-Build-Depends: debhelper (>= 3), timeout, ocaml (>= 3.06)
-
-Package: coq
-Architecture: any
-Depends: ${shlibs:Depends}
-Suggests: coq-doc, ocaml (>= 3.06), cle, ledit
-Recommends: coq-doc, proofgeneral-coq
-Description: a proof assistant for higher-order logic.
- Coq is a proof assistant for higher-order logic, which allows the
- development of computer programs consistent with their formal
- specification. It is developed using Objective Caml and Camlp4.
- For more information, see <http://coq.inria.fr/>.
-
diff --git a/distrib/debian/copyright b/distrib/debian/copyright
deleted file mode 100644
index b5d9eadf4c..0000000000
--- a/distrib/debian/copyright
+++ /dev/null
@@ -1,14 +0,0 @@
-This package was debianized by Fernando Sanchez <fer@debian.org>
-
-The "Coq proof assistant" was developed conjointly by
-        INRIA (since 1985),
-        Laboratoire de l'Informatique du Parallelisme LIP
-        associated to CNRS and ENS Lyon (sept.89-sept.97),
-        Laboratoire de Recherche en Informatique
-        associated to CNRS and Paris 11 (since sept. 97).
-
-The complete list of developpers and contributors can be found in /usr/share/doc/doc/CREDITS.gz
-
-Copyright: the Coq Proof Assistant is distributed under the terms of the GNU Lesser General Public Licence, version 2.1.
-
-See /usr/share/common-licenses/LGPL-2.1
diff --git a/distrib/debian/coq.emacsen-install b/distrib/debian/coq.emacsen-install
deleted file mode 100644
index 1ed8fe4388..0000000000
--- a/distrib/debian/coq.emacsen-install
+++ /dev/null
@@ -1,45 +0,0 @@
-#! /bin/sh -e
-# /usr/lib/emacsen-common/packages/install/coq
-
-# Written by Jim Van Zandt <jrv@vanzandt.mv.com>, borrowing heavily
-# from the install scripts for gettext by Santiago Vila
-# <sanvila@ctv.es> and octave by Dirk Eddelbuettel <edd@debian.org>.
-
-FLAVOR=$1
-PACKAGE=coq
-
-if [ ${FLAVOR} = emacs ]; then exit 0; fi
-
-echo install/${PACKAGE}: Handling install for emacsen flavor ${FLAVOR}
-
-#FLAVORTEST=`echo $FLAVOR | cut -c-6`
-#if [ ${FLAVORTEST} = xemacs ] ; then
-#    SITEFLAG="-no-site-file"
-#else
-#    SITEFLAG="--no-site-file"
-#fi
-FLAGS="${SITEFLAG} -q -batch -l path.el -f batch-byte-compile"
-
-ELDIR=/usr/share/emacs/site-lisp/${PACKAGE}
-ELCDIR=/usr/share/${FLAVOR}/site-lisp/${PACKAGE}
-
-# Install-info-altdir does not actually exist. 
-# Maybe somebody will write it.
-if test -x /usr/sbin/install-info-altdir; then
-    echo install/${PACKAGE}: install Info links for ${FLAVOR}
-    install-info-altdir --quiet --section "" "" --dirname=${FLAVOR} /usr/info/${PACKAGE}.info.gz
-fi
-
-install -m 755 -d ${ELCDIR}
-cd ${ELDIR}
-FILES=`echo *.el`
-cp ${FILES} ${ELCDIR}
-cd ${ELCDIR}
-
-cat << EOF > path.el
-(setq load-path (cons "." load-path) byte-compile-warnings nil)
-EOF
-${FLAVOR} ${FLAGS} ${FILES}
-rm -f *.el path.el
-
-exit 0
diff --git a/distrib/debian/coq.emacsen-remove b/distrib/debian/coq.emacsen-remove
deleted file mode 100644
index 02b6392ce2..0000000000
--- a/distrib/debian/coq.emacsen-remove
+++ /dev/null
@@ -1,15 +0,0 @@
-#!/bin/sh -e
-# /usr/lib/emacsen-common/packages/remove/coq
-
-FLAVOR=$1
-PACKAGE=coq
-
-if [ ${FLAVOR} != emacs ]; then
-    if test -x /usr/sbin/install-info-altdir; then
-        echo remove/${PACKAGE}: removing Info links for ${FLAVOR}
-        install-info-altdir --quiet --remove --dirname=${FLAVOR} /usr/info/coq.info.gz
-    fi
-
-    echo remove/${PACKAGE}: purging byte-compiled files for ${FLAVOR}
-    rm -rf /usr/share/${FLAVOR}/site-lisp/${PACKAGE}
-fi
diff --git a/distrib/debian/coq.emacsen-startup b/distrib/debian/coq.emacsen-startup
deleted file mode 100644
index 91b5691522..0000000000
--- a/distrib/debian/coq.emacsen-startup
+++ /dev/null
@@ -1,21 +0,0 @@
-;; -*-emacs-lisp-*-
-;;
-;; Emacs startup file for the Debian GNU/Linux coq package
-;;
-;; Originally contributed by Nils Naumann <naumann@unileoben.ac.at>
-;; Modified by Dirk Eddelbuettel <edd@debian.org>
-;; Adapted for dh-make by Jim Van Zandt <jrv@vanzandt.mv.com>
-
-;; The coq package follows the Debian/GNU Linux 'emacsen' policy and
-;; byte-compiles its elisp files for each 'emacs flavor' (emacs19,
-;; xemacs19, emacs20, xemacs20...).  The compiled code is then
-;; installed in a subdirectory of the respective site-lisp directory.
-;; We have to add this to the load-path:
-
-(setq load-path (cons (concat "/usr/share/"
-                              (symbol-name flavor)
-			      "/site-lisp/coq") load-path))
-
-(setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
-(autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t)
-
diff --git a/distrib/debian/dirs b/distrib/debian/dirs
deleted file mode 100644
index 38a404b552..0000000000
--- a/distrib/debian/dirs
+++ /dev/null
@@ -1,3 +0,0 @@
-usr/bin
-usr/lib
-usr/lib/coq
diff --git a/distrib/debian/docs b/distrib/debian/docs
deleted file mode 100644
index 62998f27c7..0000000000
--- a/distrib/debian/docs
+++ /dev/null
@@ -1,3 +0,0 @@
-README
-CREDITS
-CHANGES
diff --git a/distrib/debian/rules b/distrib/debian/rules
deleted file mode 100755
index d4e1d33768..0000000000
--- a/distrib/debian/rules
+++ /dev/null
@@ -1,89 +0,0 @@
-#!/usr/bin/make -f
-
-export DH_COMPAT=3
-
-COQPREF=$(CURDIR)/debian/coq
-ADDPREF=COQINSTALLPREFIX=${COQPREF}
-
-# in version 3.04, ocamlopt has several bugs: on some arches, it produces
-# executables that sometimes fail mysteriously or loop.
-# We use a workaround to detect this kind of situations:
-# - we try to make Coq with timeouts (TMAKE)
-# - once this is done, we check make succeeded (timeout does not
-# return the exit status of MAKE)
-#
-TMAKE=timeout 5300 ${MAKE}
-MAKEQ=${MAKE} -q
-
-CONFIGUREOPTS=--prefix /usr --mandir /usr/share/man --emacslib /usr/share/emacs/site-lisp/coq --reals all
-
-configure: configure-stamp
-configure-stamp:
-	dh_testdir
-	./configure -opt ${CONFIGUREOPTS} || ./configure ${CONFIGUREOPTS}
-	touch configure-stamp
-
-build: configure-stamp build-stamp
-build-stamp:
-	dh_testdir
-	if grep -q BEST=opt config/Makefile; \
-	then (${TMAKE} bin/coqmktop bin/coqc bin/coqtop.byte \
-	      && ${MAKEQ} bin/coqmktop bin/coqc bin/coqtop.byte \
-	      && ${TMAKE} bin/coqtop.opt bin/coqtop \
-	      && ${MAKEQ} bin/coqtop.opt bin/coqtop \
-	      && ${TMAKE} states \
-	      && ${MAKEQ} states \
-	      && ${TMAKE} world \
-	      && ${MAKEQ} world) \
-          ||  (echo WARNING: NATIVE CODE COMPILATION FAILED \
-	    && echo Trying to build coq in bytecode \
-	    && ${MAKE} archclean clean \
-	    && ${MAKE} BEST=byte world \
-	    && echo NATIVE CODE COMPILATION FAILED \
-	    && echo Coq was built in bytecode instead); \
-	else ${MAKE} world; \
-	fi
-	${MAKE} check
-	touch build-stamp
-
-clean:
-	dh_testdir
-	dh_testroot
-	rm -f build-stamp configure-stamp
-
-	-$(MAKE) clean
-	-$(MAKE) archclean
-
-	dh_clean
-
-install: build
-	dh_testdir
-	dh_testroot
-	dh_clean -k
-	dh_installdirs
-
-	$(MAKE) ${ADDPREF} install || $(MAKE) BEST=byte ${ADDPREF} install
-	-strip -R .note -R .comment ${COQPREF}/usr/bin/coqtop.opt
-
-# Build architecture-independent files here.
-binary-indep: build install
-# We have nothing to do by default.
-
-# Build architecture-dependent files here.
-binary-arch: build install
-	dh_testdir
-	dh_testroot
-	dh_installdocs
-	dh_installemacsen
-	dh_installchangelogs CHANGES
-	dh_link
-	dh_compress
-	dh_fixperms
-	dh_installdeb
-	dh_shlibdeps
-	dh_gencontrol
-	dh_md5sums
-	dh_builddeb
-
-binary: binary-indep binary-arch
-.PHONY: build clean binary-indep binary-arch binary install configure
diff --git a/distrib/petit-coq.gif b/distrib/petit-coq.gif
deleted file mode 100644
index 2d1228311b..0000000000
--- a/distrib/petit-coq.gif
+++ /dev/null
diff --git a/distrib/windows/LICENSE_SPLASH b/distrib/windows/LICENSE_SPLASH
deleted file mode 100644
index a2784d4b89..0000000000
--- a/distrib/windows/LICENSE_SPLASH
+++ /dev/null
@@ -1,5 +0,0 @@
-The splash screen is a modification a photo
- of Dave Morris (http://www.flickr.com/photos/davemorris/).
-It is distributed under the Creative Commons, 
-Attribution-NonCommercial-ShareAlike 2.0. license
-(http://creativecommons.org/licenses/by-nc-sa/2.0/).
\ No newline at end of file
diff --git a/distrib/windows/coq.nsi b/distrib/windows/coq.nsi
deleted file mode 100755
index 7c6a405705..0000000000
--- a/distrib/windows/coq.nsi
+++ /dev/null
@@ -1,259 +0,0 @@
-; This script is used to build the Windows install program for Coq.
-
-;NSIS Modern User Interface
-;Written by Joost Verburg
-;Modified by Julien Narboux
-
-; The VERSION should be passed as an argument at compile time using :
-;
-
-!define MY_PRODUCT "Coq" ;Define your own software name here
-!define EXE_PATH "..\..\bin\"
-
-!include "MUI.nsh"
-
-;--------------------------------
-;Configuration
-
-  Name "Coq"
-
-  ;General
-  OutFile "${OUTFILE}"
-
-  ;Folder selection page
-  InstallDir "$PROGRAMFILES\${MY_PRODUCT}"
-  
-  ;Remember install folder
-  InstallDirRegKey HKCU "Software\${MY_PRODUCT}" ""
-
-;Interface Configuration
-
-;  !define MUI_HEADERIMAGE
-;  !define MUI_HEADERIMAGE_BITMAP "coq_logo.bmp" ; optional
-;  !define MUI_ABORTWARNING
-
-
-;--------------------------------
-;Modern UI Configuration
-
-  !insertmacro MUI_PAGE_WELCOME
-  !insertmacro MUI_PAGE_LICENSE "..\..\LICENSE"
-  !insertmacro MUI_PAGE_COMPONENTS
-  !insertmacro MUI_PAGE_DIRECTORY
-  !insertmacro MUI_PAGE_INSTFILES
-  !insertmacro MUI_PAGE_FINISH
-  
-  !insertmacro MUI_UNPAGE_WELCOME
-  !insertmacro MUI_UNPAGE_CONFIRM
-  !insertmacro MUI_UNPAGE_INSTFILES
-  !insertmacro MUI_UNPAGE_FINISH  
-
-;--------------------------------
-;Languages
- 
-  !insertmacro MUI_LANGUAGE "English"
-  
-;--------------------------------
-;Language Strings
-
-  ;Description
-  LangString DESC_1 ${LANG_ENGLISH} "This is the windows version of Coq."
-  LangString DESC_2 ${LANG_ENGLISH} "This is CoqIde, an interactive development environment for Coq."
-  LangString DESC_3 ${LANG_ENGLISH} "This will copy the GTK dlls in the installation directory (These files are needed by CoqIde)."
-
-;--------------------------------
-;Data
-  
-Function .onInit
-  SetOutPath $TEMP
-  File /oname=coq_splash.bmp "coq_splash.bmp"
-	InitPluginsDir
-
-  advsplash::show 1000 600 400 -1 $TEMP\coq_splash
-
-  Pop $0 ; $0 has '1' if the user closed the splash screen early,
-         ; '0' if everything closed normal, and '-1' if some error occured.
-
-  Delete $TEMP\coq_splash.bmp
-FunctionEnd
-
-
-;--------------------------------
-;Installer Sections
-
-SetCompress off
-;SetCompressor bzip2
-; Comment out after debuging.
-
-Section "Coq" Sec1
-
-  ;ADD YOUR OWN STUFF HERE!
-
-  SetOutPath "$INSTDIR\"
-
-  FileOpen $0 $INSTDIR\Coq.bat w
-  FileWrite $0 "@echo off$\r$\n"
-  FileWrite $0 "set COQLIB=$INSTDIR\lib$\r$\n"
-  FileWrite $0 "set COQBIN=$INSTDIR\bin$\r$\n"
-  FileWrite $0 "set HOME=%HOMEPATH%$\r$\n"
-  FileWrite $0 "bin\coqtop.opt.exe" 
-  FileClose $0
-
-  SetOutPath "$INSTDIR\bin"
-  File /x coqide.* ${EXE_PATH}\*.exe
-  File "coq.ico"
-
-  SetOutPath "$INSTDIR\lib\theories"
-  File /r ..\..\theories\*.vo
-  SetOutPath "$INSTDIR\lib\contrib"
-  File /r ..\..\contrib\*.vo
-  SetOutPath "$INSTDIR\lib\theories7"
-  File /r ..\..\theories7\*.vo
-  SetOutPath "$INSTDIR\lib\contrib7"
-  File /r ..\..\contrib7\*.vo
-  SetOutPath "$INSTDIR\lib\states"
-  File ..\..\states\initial.coq
-  SetOutPath "$INSTDIR\lib\states7"
-  File ..\..\states7\initial.coq
-  File ..\..\states7\barestate.coq
-  SetOutPath "$INSTDIR\latex"
-  File ..\..\tools\coqdoc\coqdoc.sty
-  File ..\..\tools\coqdoc\style.css
-  SetOutPath "$INSTDIR\emacs"
-  File ..\..\tools\*.el
-  SetOutPath "$INSTDIR\man"
-  File ..\..\man\*.1
-
-  ;Store install folder
-  WriteRegStr HKCU "Software\${MY_PRODUCT}" "" $INSTDIR
-  
-  ;Create uninstaller
-  WriteUninstaller "$INSTDIR\Uninstall.exe"
-  WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
-	  "DisplayName" "Coq Version ${MY_VERSION}"
-  WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
-	  "UninstallString" '"$INSTDIR\Uninstall.exe"'
-
-  WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
-          "DisplayVersion" "${MY_VERSION}"
-
-  WriteRegDWORD HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
-          "NoModify" "1"
-  WriteRegDWORD HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
-          "NoRepair" "1"
-
-  WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
-          "URLInfoAbout" "http://coq.inria.fr"
-
-; Start Menu Entries
-
-; for the path in the .lnk
-  SetOutPath "$INSTDIR" 
-
-  CreateDirectory "$SMPROGRAMS\Coq"
-  CreateShortCut "$SMPROGRAMS\Coq\Coq.lnk" "$INSTDIR\Coq.bat" "" "$INSTDIR\bin\coq.ico" 0
-  WriteINIStr "$SMPROGRAMS\Coq\The Coq HomePage.url" "InternetShortcut" "URL" "http://coq.inria.fr"
-  WriteINIStr "$SMPROGRAMS\Coq\The Coq Standard Library.url" "InternetShortcut" "URL" "http://coq.inria.fr/library-eng.html"
-  CreateShortCut "$SMPROGRAMS\Coq\Uninstall.lnk" "$INSTDIR\Uninstall.exe" "" "$INSTDIR\Uninstall.exe" 0
-
-SectionEnd
-
-Section "CoqIde" Sec2
-
-
-  SetOutPath "$INSTDIR"
- 
-  FileOpen $0 $INSTDIR\Coqide.bat w
-  FileWrite $0 "@echo off$\r$\n"
-  FileWrite $0 "set COQLIB=$INSTDIR\lib$\r$\n"
-  FileWrite $0 "set COQBIN=$INSTDIR\bin$\r$\n"
-  FileWrite $0 "set HOME=%HOMEPATH%$\r$\n"
-  FileWrite $0 "bin\coqide.opt.exe" 
-  FileClose $0
-
-  File /oname=.coqiderc ..\..\ide\.coqide-gtk2rc
-
-  SetOutPath "$INSTDIR\bin"
-  File ${EXE_PATH}\coqide.*
-
-  ; Start Menu Entries
-  CreateShortCut "$SMPROGRAMS\Coq\CoqIde.lnk" "$INSTDIR\Coqide.bat" "" "$INSTDIR\bin\coq.ico" 0 
-
-SectionEnd
-
-Section  "The GTK DLLs (needed by CoqIde)" Sec3
-  
-  SetOutPath "$INSTDIR\bin"
-  File /r /x CVS  dlls\*.*
-
-SectionEnd
-
-;--------------------------------
-;Descriptions
-
-!insertmacro MUI_FUNCTION_DESCRIPTION_BEGIN
-  !insertmacro MUI_DESCRIPTION_TEXT ${Sec1} $(DESC_1)
-  !insertmacro MUI_DESCRIPTION_TEXT ${Sec2} $(DESC_2)
-  !insertmacro MUI_DESCRIPTION_TEXT ${Sec3} $(DESC_3)
-!insertmacro MUI_FUNCTION_DESCRIPTION_END
- 
-;--------------------------------
-;Uninstaller Section
-
-Section "Uninstall"
-
-;; Bat
-
-  Delete "$INSTDIR\Coq.bat"
-  Delete "$INSTDIR\Coqide.bat"
-
-;; We keep the settings 
-;;  Delete "$INSTDIR\.coqiderc"
- 
-;; Binaries
-  Delete "$INSTDIR\bin\*.exe"
-  Delete "$INSTDIR\bin\*.lnk"
- 
-;; Icon
-  Delete "$INSTDIR\bin\coq.ico"
-
-;; DLLs
-
-  Delete "$INSTDIR\bin\*.dll" 
-  RMDir /r "$INSTDIR\bin\etc"
-  RMDir /r "$INSTDIR\bin\lib"
-
-  RMDir "$INSTDIR\bin"
-
-;; Misc
-
-  Delete "$INSTDIR\latex\coqdoc.sty"
-  Delete "$INSTDIR\latex\style.css"
-  RMDir "$INSTDIR\latex"
-
-  Delete "$INSTDIR\man\*.1"
-  RMDir "$INSTDIR\man"
-
-  Delete "$INSTDIR\emacs\*.el"
-  RMDir "$INSTDIR\emacs"
-
-;; Lib
-
-  RMDir /r "$INSTDIR\lib"
-  
-;; Start Menu
-  Delete "$SMPROGRAMS\Coq\Coq.lnk"
-  Delete "$SMPROGRAMS\Coq\CoqIde.lnk"
-  Delete "$SMPROGRAMS\Coq\Uninstall.lnk"
-  Delete "$SMPROGRAMS\Coq\The Coq HomePage.url"
-  Delete "$SMPROGRAMS\Coq\The Coq Standard Library.url"
-  Delete "$INSTDIR\Uninstall.exe"
-  
-  DeleteRegKey /ifempty HKCU "Software\${MY_PRODUCT}"
-
-  DeleteRegKey HKEY_LOCAL_MACHINE "SOFTWARE\Coq"
-  DeleteRegKey HKEY_LOCAL_MACHINE "SOFTWARE\Microsoft\Windows\CurrentVersion\Uninstall\Coq"
-  RMDir "$INSTDIR"
-  RMDir "$SMPROGRAMS\Coq"
-
-SectionEnd
\ No newline at end of file
diff --git a/distrib/windows/coq_splash.bmp b/distrib/windows/coq_splash.bmp
deleted file mode 100755
index f7a3b42bb2..0000000000
--- a/distrib/windows/coq_splash.bmp
+++ /dev/null
diff --git a/distrib/windows/coq_splash.png b/distrib/windows/coq_splash.png
deleted file mode 100644
index 04e48bc1be..0000000000
--- a/distrib/windows/coq_splash.png
+++ /dev/null