diff options
| author | kirchner | 2004-03-26 13:21:20 +0000 |
|---|---|---|
| committer | kirchner | 2004-03-26 13:21:20 +0000 |
| commit | 352e62a650093933178251461248798821a851d8 (patch) | |
| tree | 8e375aa3f9c6ea433a8e1fd125157065d0a6bcad | |
| parent | 878e9bdf5a884a4f8cf11108c906eafc6f4de695 (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8504 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/newfaq/main.tex | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex index 7742eb7782..d941be5031 100644 --- a/doc/newfaq/main.tex +++ b/doc/newfaq/main.tex @@ -152,13 +152,13 @@ The first official release of \Coq (v. 4.1.0) was distributed in 1989. \begin{description} \item[Coqide] A GTK based gui for \Coq. \item[Pcoq] A gui for \Coq with proof by pointing and pretty printing. -\item[Why] -\item[Krakatoa] +\item[Why] A back-end generator of verification conditions. +\item[Krakatoa] A Java code certification tool that uses both Coq and Why to verify the soundness of implementations with regards to the specifications. \item[coqwc] A tool similar to {\tt wc} to count lines in \Coq files. \item[coq-tex] A tool to insert \Coq examples within .tex files. \item[coqdoc] A documentation tool for \Coq. \item[Proof General] A emacs mode for \Coq and many other proof assistants. -\item[Foc] +\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 ?} @@ -205,8 +205,7 @@ The goal is the statement to be proved. \Question[dependanttype]{What is a dependent type ?} - -\Question[conjonction]{My goal is a conjonction, how can I prove it ?} +\Question[conjonction]{My goal is a conjunction, how can I prove it ?} Use some theorem or assumption or use the {\tt split} tactic. |