MAJ Search

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

1 files changed, 5 insertions, 11 deletions

diff --git a/doc/RefMan-oth.tex b/doc/RefMan-oth.tex
index 1018ca460e..91b89650b0 100644
--- a/doc/RefMan-oth.tex
+++ b/doc/RefMan-oth.tex
@@ -170,26 +170,20 @@ SearchRewrite (plus ? ?).
 
 \begin{Variants}
 \item
- {\tt Search {\qualid} inside
+{\tt Search {\qualid} inside
 {\module$_1$}...{\module$_n$}.}\comindex{Search ... inside ...}\\
 {\tt SearchPattern {\term} inside
 {\module$_1$}...{\module$_n$}.}\comindex{SearchPattern ... inside
 ...}\\
 {\tt SearchRewrite {\term} inside
-{\module$_1$}...{\module$_n$}.}\comindex{SearchRewrite ... inside ...}\\
+{\module$_1$}...{\module$_n$}.}\comindex{SearchRewrite ... inside ...}
+
 This restricts the search to constructions defined in modules {\module$_1$}...{\module$_n$}.
 
 \item {\tt Search {\qualid} outside {\module$_1$}...{\module$_n$}.}\comindex{Search ... outside ...}\\
-  This restricts the search to constructions not defined in modules {\module$_1$}...{\module$_n$}.
-
-
-  This restricts the search to constructions defined in modules {\module$_1$}...{\module$_n$}.
-
-\item {\tt SearchPattern {\term} outside {\module$_1$}...{\module$_n$}.}\comindex{SearchPattern ... outside ...}\\
-  This restricts the search to constructions not defined in modules
-{\module$_1$}...{\module$_n$}.
+{\tt SearchPattern {\term} outside {\module$_1$}...{\module$_n$}.}\comindex{SearchPattern ... outside ...}\\
+{\tt SearchRewrite {\term} outside {\module$_1$}...{\module$_n$}.}\comindex{SearchRewrite ... outside ...}
 
-\item {\tt SearchRewrite {\term} outside {\module$_1$}...{\module$_n$}.}\comindex{SearchRewrite ... outside ...}\\
   This restricts the search to constructions not defined in modules
 {\module$_1$}...{\module$_n$}.