maj de la faq: correction de l'exemple field qui compilait plus en 8.2, correction de quelques typos, maj des <<related tools>>, suppression des questions sans reponse

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

1 files changed, 25 insertions, 16 deletions

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index a21de8f24..4309926b9 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -286,6 +286,8 @@ There are graphical user interfaces:
 \item[Pcoq] A GUI for {\Coq} with proof by pointing and pretty printing.
 \item[coqwc] A tool similar to {\tt wc} to count lines in {\Coq} files.
 \item[Proof General] A emacs mode for {\Coq} and many other proof assistants.
+\item[ProofWeb] The ProofWeb online web interface for {\Coq} (and other proof assistants), with a focus on teaching. 
+\item[ProverEditor] is an experimental Eclipse plugin with support for {\Coq}. 
 \end{description}
 
 There are documentation and browsing tools:
@@ -294,6 +296,7 @@ There are documentation and browsing tools:
 \item[Helm/Mowgli] A rendering, searching and publishing tool.
 \item[coq-tex] A tool to insert {\Coq} examples within .tex files. 
 \item[coqdoc] A documentation tool for \Coq.
+\item[coqgraph] A tool to generate a dependency graph from {\Coq} sources.
 \end{description}
 
 There are front-ends for specific languages:
@@ -304,6 +307,9 @@ There are front-ends for specific languages:
 \item[Caduceus] A C code certification tool that uses both {\Coq} and \Why.
 \item[Zenon] A first-order theorem prover.
 \item[Focal] The \ahref{http://focal.inria.fr}{Focal} project aims at building an environment to develop certified computer algebra libraries. 
+\item[Concoqtion] is a dependently-typed extension of Objective Caml (and of MetaOCaml) with specifications expressed and proved in Coq. 
+\item[Ynot] is an extension of Coq providing a "Hoare Type Theory" for specifying higher-order, imperative and concurrent programs.
+\item[Ott]is a tool to translate the descriptions of the syntax and semantics of programming languages to the syntax of Coq, or of other provers.
 \end{description}
 
 \Question{What are the high-level tactics of \Coq}
@@ -369,7 +375,7 @@ This FAQ is available online at \ahref{http://coq.inria.fr/doc/faq.html}{\url{ht
 \Question{How can I submit suggestions / improvements / additions for this FAQ?}
 
 This FAQ is unfinished (in the sense that there are some obvious
-sections that are missing). Please send contributions to \texttt{Florent.Kirchner at lix.polytechnique.fr} and \texttt{Julien.Narboux at inria.fr}.
+sections that are missing). Please send contributions to Coq-Club.
 
 \Question{Is there any mailing list about {\Coq}?} 
 The main {\Coq} mailing list is \url{coq-club@pauillac.inria.fr}, which
@@ -1124,7 +1130,11 @@ Open Local Scope R_scope.
 Goal forall a b : R, b*a<>0 -> (a/b) * (b/a) = 1. 
 intros.
 field.
-assumption.
+cut (b*a <>0 -> a<>0).
+cut (b*a <>0 -> b<>0).
+auto.
+auto with real.
+auto with real.
 Qed.
 \end{coq_example}
 
@@ -1204,13 +1214,9 @@ Perhaps you may need to use \eauto.
 
 This is the same tactic as \auto, but it relies on {\eapply} instead of \apply.
 
-\iffalse
-todo les espaces
-\fi
-
 \Question{How can I speed up {\auto}?}
 
-You can use \texttt{info }\auto to replace {\auto} by the tactics it generates.
+You can use \texttt{info }{\auto} to replace {\auto} by the tactics it generates.
 You can split your hint bases into smaller ones.
 
 
@@ -1416,6 +1422,7 @@ You can use the {\tt Clear} command.
 \Question{How can use a proof which is not finished?}
 
 You can use the {\tt Admitted} command to state your current proof as an axiom.
+You can use the {\tt admit} tactic to omit a portion of a proof.
 
 \Question{How can I state a conjecture?}
 
@@ -1892,9 +1899,6 @@ You can do ``Print Grammar constr'', and decode the output from camlp4, good luc
 {\Ltac} is the tactic language for \Coq. It provides the user with a
 high-level ``toolbox'' for tactic creation.
 
-\Question{Why do I always get the same error message?}
-
-
 \Question{Is there any printing command in {\Ltac}?}
 
 You can use the {\idtac} tactic with a string argument. This string
@@ -1971,7 +1975,9 @@ You can use typeof.
 todo
 \fi
 
+\iffalse
 \Question{How can I define static and dynamic code?}
+\fi
 
 \section{Tactics written in Ocaml}
 
@@ -1984,8 +1990,10 @@ You have some examples of tactics written in Ocaml in the ``contrib'' directory
 
 \section{Case studies}
 
-
+\iffalse
 \Question{How can I define vectors or lists of size n?}
+\fi
+
 
 \Question{How to prove that 2 sets are different?}
 
@@ -2204,7 +2212,8 @@ You can use {\tt coqdoc}.
 
 \Question{How can I generate some dependency graph from my development?}
 
-You can use {\tt coq\_tex}.
+You can use the tool \verb|coqgraph| developped by Philippe Audebaud in 2002.
+This tool transforms dependancies generated by \verb|coqdep| into 'dot' files which can be visualized using the Graphviz software (http://www.graphviz.org/).
 
 \Question{How can I cite some {\Coq} in my latex document?}
 
@@ -2218,8 +2227,8 @@ You can use this bibtex entry:
   title =        {The Coq proof assistant reference manual},
   author =       {\mbox{The Coq development team}},
   organization = {LogiCal Project},
-  note =         {Version 8.0},
-  year =         {2004},
+  note =         {Version 8.2},
+  year =         {2009},
   url =          "http://coq.inria.fr"
 }
 \end{verbatim}
@@ -2417,7 +2426,7 @@ internal reduction of {\Coq} (not using the tactic language of {\Coq}
 (\Ltac) nor the implementation language for \Coq).  An example of
 tactic using the reflection mechanism is the {\ring} tactic. The
 reflection method consist in reflecting a subset of {\Coq} language (for
-example the arithmetical expressions) into an object of the \Coq
+example the arithmetical expressions) into an object of the {\Coq}
 language itself (in this case an inductive type denoting arithmetical
 expressions).  For more information see~\cite{howe,harrison,boutin}
 and the last chapter of the Coq'Art.
@@ -2446,7 +2455,7 @@ stated some local lemma, this speeds up the typing process.
 
 \Question{Why \texttt{Reset Initial.} does not work when using \texttt{coqc}?}
 
-The initial state corresponds to the state of coqtop when the interactive
+The initial state corresponds to the state of \texttt{coqtop} when the interactive
 session began. It does not make sense in files to compile.