diff options
| author | narboux | 2004-04-02 10:42:48 +0000 |
|---|---|---|
| committer | narboux | 2004-04-02 10:42:48 +0000 |
| commit | e271ac3bdba982887d2fe0a97484e8289305f4fd (patch) | |
| tree | 754cac7608a5fb837e3b991ebc7a5d2b30295528 /doc | |
| parent | d5442f9a05c87295a3bb46409a228ba73c11da8f (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8526 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/newfaq/main.tex | 10 |
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} |
