diff options
Diffstat (limited to 'doc/newfaq/main.tex')
| -rw-r--r-- | doc/newfaq/main.tex | 20 |
1 files changed, 16 insertions, 4 deletions
diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex index d941be503..5e5378854 100644 --- a/doc/newfaq/main.tex +++ b/doc/newfaq/main.tex @@ -122,6 +122,12 @@ downloadable postscripts. \Question[coqfaq]{Where can I find this faq on the web ?} Errr\ldots + +\Question[faqimprov]{How can I submit suggestions/improvements/additions for this FAQ?} + +This FAQ is unfinished (in the sense that there are some obvious sections it needs, some included below). Please send contributions to the authors. + + \Question[coqmailinglist]{Is there any mailing list about \Coq ?} The main \Coq mailing list is {\tt coq-club@pauillac.inria.fr}, which broadcasts questions and suggestions about the implementation, the @@ -130,6 +136,8 @@ logical formalism or proof developments. See subsription. Bugs reports should be sent at the {\tt coq-bugs@pauillac.inria.fr} mailing-list. +\Question[coqmailinglistarchive]{Where can I find an archive of the list?} + \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: @@ -141,12 +149,17 @@ students, and engineers interested in formal methods and the development of zero-default software.'' \end{quote} +\Question[coqbug]{How can I report a bug ?} + + + \Question[nbusers]{How many \Coq users are there ?} \Question[howold]{How old is \Coq ?} The first official release of \Coq (v. 4.1.0) was distributed in 1989. + \Question[relatedtools]{What are the \Coq-related tools ?} \begin{description} @@ -161,7 +174,7 @@ The first official release of \Coq (v. 4.1.0) was distributed in 1989. \item[Foc] The Foc project aims at building an environment to develop certified computer algebra libraries. \end{description} -\Question[indutrial]{What are industrial application for \Coq ?} +\Question[industrial]{What are industrial application for \Coq ?} Trusted Logic ... @@ -303,10 +316,9 @@ For more information see \cite{howe,harrison,boutin} and the last chapter of th \Question[ltacprint]{Is there any printing command in \Ltac ?} -You can use the {\tt Idtac} tactic with a string argument. Thsi string +You can use the {\tt Idtac} tactic with a string argument. This string will be printed out. -The same applies to the -{\tt fail} tactic +The same applies to the {\tt fail} tactic \Question[letltac]{What is the syntax for let in \Ltac ?} |