diff options
| -rw-r--r-- | doc/newfaq/main.tex | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex index d3a408a1e6..c71a3b12c6 100644 --- a/doc/newfaq/main.tex +++ b/doc/newfaq/main.tex @@ -143,8 +143,8 @@ Coq is used by Trusted Logic to prove properties of the JavaCard system. \section{Documentation} \Question[coqdocumentation]{Where can I find documentation about \Coq ?} -All the documentation about \Coq, from the reference manual \cite{Coq:manual} to -friendly tutorials \cite{Coq:Tutorial} and documentation of the standard library, is available online at +All the documentation about \Coq, from the reference manual~\cite{Coq:manual} to +friendly tutorials~\cite{Coq:Tutorial} and documentation of the standard library, is available online at \url{http://pauillac.inria.fr/coq/doc-eng.html}. All these documents are viewable either in browsable html, or as downloadable postscripts. @@ -181,7 +181,7 @@ development of zero-default software.'' \Question[coqexamples]{Where can I find some \Coq examples ?} -There are examples in the manual \cite{Coq:manual} and in the CoqArt \cite{Coq:coqart}. You can also find large developments using \Coq in the \Coq user contributions : \url{http://coq.inria.fr/distrib-eng.html} +There are examples in the manual~\cite{Coq:manual} and in the Coq'Art~\cite{Coq:coqart}. You can also find large developments using \Coq in the \Coq user contributions : \url{http://coq.inria.fr/distrib-eng.html} \Question[coqbug]{How can I report a bug ?} @@ -345,7 +345,7 @@ The goal is the statement to be proved. This is a proof generated by some computation which is done using the 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 {\tt ring} tactic. The reflection method consist in reflecting a subset of Coq language (for example the arithmetical expressions) into an object of the Coq language itself (in our case an inductive type denoting arithmetical expressions). -For more information see \cite{howe,harrison,boutin} and the last chapter of the CoqArt. +For more information see~\cite{howe,harrison,boutin} and the last chapter of the Coq'Art. \section{Conclusion and Farewell.} |