aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authornarboux2004-04-02 10:42:48 +0000
committernarboux2004-04-02 10:42:48 +0000
commite271ac3bdba982887d2fe0a97484e8289305f4fd (patch)
tree754cac7608a5fb837e3b991ebc7a5d2b30295528
parentd5442f9a05c87295a3bb46409a228ba73c11da8f (diff)
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8526 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--doc/newfaq/main.tex10
1 files changed, 8 insertions, 2 deletions
diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index c1476d40cf..b52a6ac6b2 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -114,7 +114,8 @@ The Coq tool is a proof assistant which:
\item helps to find formal proofs,
\item extracts a certified program from the constructive proof of its formal specification,
\end{itemize}
-Coq is written in the Objective Caml language and uses the Camlp4 Pre-processor-pretty-printer for Objective Caml.
+Coq is written in the Objective Caml language and uses
+the Camlp4 Pre-processor-pretty-printer for Objective Caml.
\Question[name]{Did you really need to name it like that ?}
Some French computer scientists have a tradition of naming their
@@ -210,6 +211,12 @@ subsription. Bugs reports should be sent at
The archives of the \Coq mailing list are available at
\url{http://pauillac.inria.fr/pipermail/coq-club}.
+
+\Question[newversion]{How can I be kept informed of new releases of \Coq ?}
+
+New versions of \Coq are annonced on the coq-club mailing list. If you only want to receive information about new releases, you can subscribe to \Coq on \url{www.freashmeat.net}.
+
+
\Question[coqbook]{Is there any book about \Coq ?}
The first book on \Coq, Yves Bertot and Pierre Castéran's Coq'Art will
be published by Springer-Verlag in 2004:
@@ -250,7 +257,6 @@ be accessed via anonymous CVS: \url{http://coqcvs.inria.fr/cvsserver-eng.html}
Compiled binaries are available for Linux, MacOs X, Solaris, and
Windows. The sources can be easily adapted to all platforms supporting Objective Caml.
-
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Talkin' with the Rooster}