Orthographe

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

3 files changed, 12 insertions, 9 deletions

diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex
index 5fc9aac26..aece35fe8 100644
--- a/doc/RefMan-ext.tex
+++ b/doc/RefMan-ext.tex
@@ -508,7 +508,7 @@ Note the difference between the value of {\tt x'} inside section {\tt
 \item Most commands, like {\tt Hint \ident} or {\tt Syntactic
   Definition} which appear inside a section are cancelled when the
 section is closed.
-% See \ref{LongNames}
+% cf section \ref{LongNames}
 %\item Usually all identifiers must be distinct. 
 %However, a name already used in a closed section (see \ref{Section})
 %can be reused. In this case, the old name is no longer accessible.
@@ -520,7 +520,8 @@ section is closed.
 
 \section{Libraries and long names}
 \label{LongNames}
-
+\index{Qualified identifiers}
+\index{Absolute names}
 \paragraph{Libraries}
 
 The theories developed in {\Coq} are stored in {\em libraries}.  A
@@ -553,7 +554,7 @@ operating system using the command (see \ref{AddLoadPath})
 \end{quote}
 
 A library can inherit the tree structure of a physical directory by
-using the {\tt -R} option to {\tt coqtop} (see \ref{coqtop}) or the
+using the {\tt -R} option to {\tt coqtop} or the
 command (see \ref{AddRecLoadPath})
 
 \begin{quote}
@@ -643,7 +644,7 @@ physical file \verb!theories/Init/Datatypes.vo! in {\Coq} installation directory
 When requiring the file, the mapping between physical directories and logical library should be consistent with the mapping used to compile the file (for modules of the standard library, this is automatic -- check it by typing {\tt Print LoadPath}).
 
 The command {\tt Add Rec LoadPath} is also available from {\tt coqtop}
-and {\tt coqc} by using option~\verb=-R= (see section \ref{Tools}).
+and {\tt coqc} by using option~\verb=-R=.
 
 \section{Implicit arguments}\index{implicit arguments}
 
@@ -907,8 +908,8 @@ To skip the printing of coercions, use
 By default, coercions are not printed.
 
 \subsubsection{\tt Set Printing Coercion {\qualid}.}
-\comindex{Set Printing Coercions}
-\comindex{Unset Printing Coercions}
+\comindex{Set Printing Coercion}
+\comindex{Unset Printing Coercion}
 
 This command forces coercion denoted by {\qualid} to be printed.
 To skip the printing of coercion {\qualid}, use
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex
index e74d286d2..e998b8488 100644
--- a/doc/RefMan-gal.tex
+++ b/doc/RefMan-gal.tex
@@ -875,7 +875,7 @@ It is also possible to parameterize these inductive definitions.
 However, parameters correspond to a local
 context in which the whole set of inductive declarations is done.  For
 this reason, the parameters must be strictly the same for each
-inductive types The extented syntax is:
+inductive types The extended syntax is:
 
 \medskip
 {\tt 
diff --git a/doc/RefMan-oth.tex b/doc/RefMan-oth.tex
index e127a0d79..5beb3d78d 100644
--- a/doc/RefMan-oth.tex
+++ b/doc/RefMan-oth.tex
@@ -444,7 +444,9 @@ which can be any valid path.
   Is equivalent to {\tt Pwd.}
 \end{Variants}
 
-\subsection{\tt Add LoadPath {\str} as {\dirpath}.}\comindex{Add LoadPath}
+\subsection{\tt Add LoadPath {\str} as {\dirpath}.}
+\comindex{Add LoadPath}\label{AddLoadPath}
+
 This command adds the path {\str} to the current \Coq\ loadpath and
 maps it to the logical directory {\dirpath}, which means that every
 file {\tt M.v} physically lying in directory {\str} will be considered
@@ -455,7 +457,7 @@ as a module of logical name ``{\dirpath}{\tt{.M}}''.
 Performs as {\tt Add LoadPath {\str} as {\dirpath}.} but for an empty directory path.
 \end{Variants}
 
-\subsection{\tt Add Rec LoadPath {\str} as {\dirpath}.}\comindex{Add Rec LoadPath}
+\subsection{\tt Add Rec LoadPath {\str} as {\dirpath}.}\comindex{Add Rec LoadPath}\label{AddRecLoadPath}
 This command adds the directory {\str} and all its subdirectories 
 to the current \Coq\ loadpath. The top directory {\str} is mapped to the logical directory {\dirpath}, any subdirectory {\textsl{pdir}} will be mapped to logical directory {\dirpath}{\tt{.pdir}} and so on.