remove old traces of SearchIsos (never ported to 7.x nor 8.x)

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

5 files changed, 2 insertions, 64 deletions

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index aaa962570..22417d60e 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -34,11 +34,6 @@ toplevel (to allow the dynamic link of tactics).  You can switch to
 the Caml toplevel with the command \verb!Drop.!, and come back to the
 \Coq~toplevel with the command \verb!Toplevel.loop();;!.
 
-% The command \verb!coqtop -searchisos! runs the search tool {\sf
-%   Coq\_SearchIsos} (see Section~\ref{coqsearchisos},
-% page~\pageref{coqsearchisos}) and, as the \Coq~system, can be combined
-% with the option \verb!-opt!.
-
 \section{Batch compilation ({\tt coqc})}
 The {\tt coqc} command takes a name {\em file} as argument.  Then it
 looks for a vernacular file named {\em file}{\tt .v}, and tries to
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 5a564b676..e2841ad64 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -336,16 +336,6 @@ This restricts the search to constructions not defined in modules
 
 \end{Variants}
 
-% \subsection[\tt SearchIsos {\term}.]{\tt SearchIsos {\term}.\comindex{SearchIsos}}
-% \label{searchisos}
-% \texttt{SearchIsos} searches terms by their type modulo isomorphism.
-% This command displays the full name of all constants, variables,
-% inductive types, and inductive constructors of the current
-% context whose type is isomorphic to {\term} modulo the contextual part of the
-% following axiomatization (the mutual inductive types with one constructor,
-% without implicit arguments, and for which projections exist, are regarded as a
-% sequence of $\sa{}$):
-
 
 % \begin{tabbing}
 % \ \ \ \ \=11.\ \=\kill
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 996a15cd4..8a3a1f6d4 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -125,44 +125,6 @@ subdirectories. For more options type
 the sources of \Coq{} somewhere and have an environment variable named
 \texttt{COQTOP} that points to that directory.
 
-% \section{{\sf Coq\_SearchIsos}: information retrieval in a \Coq\ proofs
-% library}
-% \label{coqsearchisos}
-% \index{Coq\_SearchIsos@{\sf Coq\_SearchIsos}}
-
-% In the \Coq\ distribution, there is also a separated and independent tool,
-% called {\sf Coq\_SearchIsos}, which allows the search in accordance with {\tt
-% SearchIsos}\index{SearchIsos@{\tt SearchIsos}} (see Section~\ref{searchisos})
-% in a \Coq\ proofs library. More precisely, this program begins, once launched
-% by {\tt coqtop -searchisos}\index{coqtopsearchisos@{\tt
-% coqtop -searchisos}}, loading lightly (by using specifications functions)
-% all the \Coq\ objects files ({\tt .vo}) accessible by the {\tt LoadPath} (see
-% Section~\ref{loadpath}). Next, a prompt appears and four commands are then
-% available:
-
-% \begin{description}
-% \item [{\tt SearchIsos}]\ \\
-%   Scans the fixed context.
-% \item [{\tt Time}]\index{Time@{\tt Time}}\ \\
-%   Turns on the Time Search Display mode (see Section~\ref{time}).
-% \item [{\tt Untime}]\index{Untime@{\tt Untime}}\ \\
-%   Turns off the Time Search Display mode (see Section~\ref{time}).
-% \item [{\tt Quit}]\index{Quit@{\tt Quit}}\ \\
-%   Ends the {\tt coqtop -searchisos} session.
-% \end{description}
-
-% When running {\tt coqtop -searchisos} you can use the two options:
-
-% \begin{description}
-% \item[{\tt -opt}]\ \\
-%   Runs the native-code version of {\sf Coq\_SearchIsos}.
-
-% \item[{\tt -image} {\em file}]\ \\
-%   This option sets the binary image to be used to be {\em file}
-%   instead of the standard one. Not of general use.
-% \end{description}
-
-
 \section[Documenting \Coq\ files with coqdoc]{Documenting \Coq\ files with coqdoc\label{coqdoc}
 \index{Coqdoc@{\sf coqdoc}}}
 
diff --git a/man/coqmktop.1 b/man/coqmktop.1
index cae9f1e84..810df782c 100644
--- a/man/coqmktop.1
+++ b/man/coqmktop.1
@@ -50,10 +50,6 @@ Build Coq on a ocaml toplevel (incompatible with
 .BR \-opt )
 
 .TP
-.B \-searchisos
-Build a toplevel for SearchIsos
-
-.TP
 .BI \-R \ dir
 Specify recursively directories for Ocaml
 
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 0ff487fb4..14f26582f 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -49,7 +49,6 @@ let notopobjs = gramobjs
 let opt        = ref false
 let full       = ref false
 let top        = ref false
-let searchisos = ref false
 let echo       = ref false
 
 let src_dirs () =
@@ -133,7 +132,6 @@ let usage () =
 \n  -echo          Print calls to external commands\
 \n  -full          Link high level tactics\
 \n  -opt           Compile in native code\
-\n  -searchisos    Build a toplevel for SearchIsos\
 \n  -top           Build Coq on a OCaml toplevel (incompatible with -opt)\
 \n  -R dir         Specify recursively directories for Ocaml\
 \n";
@@ -239,11 +237,8 @@ let create_tmp_main_file modules =
     output_string oc "\"];;\n";
     (* Initializes the kind of loading *)
     output_string oc (declare_loading_string());
-    (* Start the right toplevel loop: Coq or Coq_searchisos *)
-    if !searchisos then
-      output_string oc "Cmd_searchisos_line.start();;\n"
-    else
-      output_string oc "Coqtop.start();;\n";
+    (* Start the toplevel loop *)
+    output_string oc "Coqtop.start();;\n";
     close_out oc;
     main_name
   with e ->