From 65a8a6782dcea646100be18d993f244d3dbe86f4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 18 Dec 2000 23:33:17 +0000
Subject: MAJ Search

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8153 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-oth.tex | 16 +++++-----------
 1 file changed, 5 insertions(+), 11 deletions(-)

(limited to 'doc/RefMan-oth.tex')

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$}.
 
-- 
cgit v1.2.3