diff options
| author | marche | 2003-12-19 09:19:09 +0000 |
|---|---|---|
| committer | marche | 2003-12-19 09:19:09 +0000 |
| commit | 99e2f370a25f126f036b2910d4b919951002fb91 (patch) | |
| tree | bc19463d6b931d6277beeb49c195e34af78dbea6 /doc/RefMan-lib.tex | |
| parent | a1fa5ceaf8e084411ce60bf5e38b24ee4e857f6d (diff) | |
COQBIN plus necessaire, typos
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8417 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/RefMan-lib.tex')
| -rwxr-xr-x | doc/RefMan-lib.tex | 29 |
1 files changed, 11 insertions, 18 deletions
diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex index 757a0e2ce5..b147fd659e 100755 --- a/doc/RefMan-lib.tex +++ b/doc/RefMan-lib.tex @@ -974,10 +974,8 @@ intros; split_Rmult. \end{coq_example} All this tactics has been written with the tactic language Ltac -described in chapter~\ref{TacticLanguage}.\\ - -More details are available in this document: {\tt -http://coq.inria.fr/$\sim$desmettr/Reals.ps}.\\ +described in chapter~\ref{TacticLanguage}. More details are available +in document \url{http://coq.inria.fr/~desmettr/Reals.ps}. \begin{coq_eval} Reset Initial. @@ -995,26 +993,21 @@ can be accessed by requiring module {\tt List}. \index{Contributions} \label{Contributions} -Numerous users' contributions have been collected and are available on -the WWW at the following address: \verb!coq.inria.fr/contribs/!. -On this web page, you have a list of all contributions with -informations (author, institution, quick description, etc.) and the -possibility to download them one by one. -There is a small search engine to look for keywords in all contributions. -You will also find informations on how to submit a new contribution. +Numerous users' contributions have been collected and are available at +URL \url{coq.inria.fr/contribs/}. On this web page, you have a list +of all contributions with informations (author, institution, quick +description, etc.) and the possibility to download them one by one. +There is a small search engine to look for keywords in all +contributions. You will also find informations on how to submit a new +contribution. The users' contributions may also be obtained by anonymous FTP from site \verb:ftp.inria.fr:, in directory \verb:INRIA/coq/: and -searchable on-line at - -\begin{quotation} - \texttt{http://coq.inria.fr/contribs-eng.html} -\end{quotation} +searchable on-line at \url{http://coq.inria.fr/contribs-eng.html} % $Id$ - %%% Local Variables: %%% mode: latex -%%% TeX-master: t +%%% TeX-master: "Reference-Manual" %%% End: |