relecture JCF

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

3 files changed, 5 insertions, 27 deletions

diff --git a/doc/RefMan-oth.tex b/doc/RefMan-oth.tex
index 3dc852cd0f..d420a269af 100644
--- a/doc/RefMan-oth.tex
+++ b/doc/RefMan-oth.tex
@@ -58,12 +58,6 @@ was introduced.
 This command displays the type of {\term}. When called in proof mode, 
 the term is checked in the local context of the current subgoal.
 
-\begin{Variants}
-\item \texttt{Check {\num} {\term}}\\
-  Displays the type of {\term} in the context of the {\num}-th
-  subgoal.
-\end{Variants}
-
 \subsection{\tt Eval {\rm\sl convtactic} in {\term}.}
 \comindex{Eval}
 
@@ -72,11 +66,6 @@ the resulting term with its type. The term to be reduced may depend on
 hypothesis introduced in the first subgoal (if a proof is in
 progress).
 
-\begin{Variants}
-\item \texttt{Eval {\num} {\rm\sl convtactic} in {\term}.}\\
-  Evaluates {\term} in the context of the {\num}-th subgoal.
-\end{Variants}
-
 \SeeAlso section~\ref{Conversion-tactics}.
 
 \subsection{\tt Extraction \term.}
@@ -210,8 +199,8 @@ SearchAbout [ Zmult Zplus "distr" ].
 \end{coq_example}
 
 \item
-{\tt SearchAbout {\term} outside {\module$_1$}...{\module$_n$}.}\\
-{\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{} ] outside {\module$_1$}...{\module$_n$}.}
+{\tt SearchAbout {\term} inside {\module$_1$}...{\module$_n$}.}\\
+{\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{} ] inside {\module$_1$}...{\module$_n$}.}
 
 This restricts the search to constructions defined in modules
 {\module$_1$}...{\module$_n$}.
@@ -436,17 +425,6 @@ waste of time.
 TODO + variant Export
 
 
-
-\subsection{\tt Read Module {\qualid}.}\comindex{Read Module}
-This looks for a physical file \texttt{file.vo} mapped to logical name
-{\qualid} in the current {\Coq} loadpath, then loads its contents but
-does not open it: its contents remains accesible to the user only by
-using names prefixed by the module name (i.e. {\qualid} or any other
-qualified names denoting the same module).
-%  The implementation file
-% ({\ident}{\tt.vo}) is searched first, then the specification file
-% ({\ident}{\tt.vi}) in case of failure.
-
 \subsection{\tt Require {\dirpath}.}
 \label{Require}
 \comindex{Require}
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 0639ff8b80..e29b37bf88 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -1791,7 +1791,7 @@ incompatibilities.
 
 \SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_tauto.v}
 
-\subsection{{\tt Firstorder}}\tacindex{Firstorder}}
+\subsection{{\tt Firstorder}\tacindex{Firstorder}}
 \label{Firstorder}
 
 The tactic Firstorder is an {\it experimental} extension of Tauto to 
diff --git a/doc/RefMan.txt b/doc/RefMan.txt
index f50f86bfdd..ccaa488b83 100644
--- a/doc/RefMan.txt
+++ b/doc/RefMan.txt
@@ -19,10 +19,10 @@ MANUEL DE REFERENCE
 
 
 \part{The proof engine}
-\include{RefMan-oth.v}% Vernacular commands			JCF
+\include{RefMan-oth.v}% Vernacular commands			JCF -fait
 \include{RefMan-pro}% Proof handling				Clement
 \include{RefMan-tac.v}% Tactics and tacticals			JCF
-%% ajouter JProver/Ground/CC					Pierre C
+%% ajouter JProver/Ground/CC					Pierre C -fait
 \include{RefMan-tacex.v}% Detailed Examples of tactics		JCF
 
 \part{User extensions}