diff options
| -rw-r--r-- | distrib/MacOS-X/Licence.rtf.template | 30 | ||||
| -rw-r--r-- | distrib/MacOS-X/ReadMe.rtf.template | 30 | ||||
| -rw-r--r-- | distrib/MacOS-X/Welcome.rtf.template | 5 |
3 files changed, 41 insertions, 24 deletions
diff --git a/distrib/MacOS-X/Licence.rtf.template b/distrib/MacOS-X/Licence.rtf.template index 3c50b3024e..c0b43e7f03 100644 --- a/distrib/MacOS-X/Licence.rtf.template +++ b/distrib/MacOS-X/Licence.rtf.template @@ -4,12 +4,16 @@ \margl1440\margr1440\vieww9600\viewh15620\viewkind0 \pard\tx1440\tx2880\tx4320\tx5760\tx7200\ql\qnatural -\f0\fs24 \cf0 Coq VVERSION is released under the terms of the GNU Less\ -General Public Licence, version 2.1 (included below).\ +\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\ + 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\ @@ -20,7 +24,7 @@ General Public Licence, version 2.1 (included below).\ as the successor of the GNU Library Public License, version 2, hence\ the version number 2.1.]\ \ - Preamble\ + Preamble\ \ The licenses for most software are designed to take away your\ freedom to share and change it. By contrast, the GNU General Public\ @@ -35,7 +39,7 @@ 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\ +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\ @@ -91,15 +95,15 @@ 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\ +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\ +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.\ @@ -122,7 +126,7 @@ modification follow. Pay close attention to the difference between a\ 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\ + GNU LESSER GENERAL PUBLIC LICENSE\ TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION\ \ 0. This License Agreement applies to any software library or other\ @@ -442,7 +446,7 @@ 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\ + 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.\ @@ -465,7 +469,7 @@ 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\ + END OF TERMS AND CONDITIONS\ \ How to Apply These Terms to Your New Libraries\ \ diff --git a/distrib/MacOS-X/ReadMe.rtf.template b/distrib/MacOS-X/ReadMe.rtf.template index 4ec8f14881..8d418d5b4e 100644 --- a/distrib/MacOS-X/ReadMe.rtf.template +++ b/distrib/MacOS-X/ReadMe.rtf.template @@ -4,14 +4,28 @@ \margl1440\margr1440\vieww9000\viewh9000\viewkind0 \pard\tx1440\tx2880\tx4320\tx5760\tx7200\ql\qnatural -\f0\fs24 \cf0 Developped in the INRIA LogiCal project, The Coq tool is a proof\ -assistant which:\ +\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:\ \ -- allows to handle calculus assertions,\ -- allows to check mechanically proofs of these assertions,\ -- helps to find formal proofs,\ -- extracts a certified program from the constructive proof of its formal specification,\ +- 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 written in the Objective Caml language and uses the Camlp4\ -Pre-processor-pretty-printer for Objective Caml.\ +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)\ +- 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 index ed843ef5bb..8925f1dfb5 100644 --- a/distrib/MacOS-X/Welcome.rtf.template +++ b/distrib/MacOS-X/Welcome.rtf.template @@ -4,8 +4,7 @@ \margl1440\margr1440\vieww9000\viewh9000\viewkind0 \pard\tx1440\tx2880\tx4320\tx5760\tx7200\ql\qnatural -\f0\fs24 \cf0 This package will install the binary distribution of Coq VVERSION on\ -your Macintosh.\ +\f0\fs24 \cf0 This package will install the MacOS X binary distribution of Coq VVERSION.\ \ -You will need 41 MB of disk space to install this package.\ +You will need about 30MB of disk space to install this package.\ } |