From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 28 Apr 2006 14:59:16 +0000
Subject: Imported Upstream version 8.0pl3+8.1alpha

---
 doc/refman/RefMan-oth.tex | 773 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 773 insertions(+)
 create mode 100644 doc/refman/RefMan-oth.tex

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

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
new file mode 100644
index 00000000..e92cde74
--- /dev/null
+++ b/doc/refman/RefMan-oth.tex
@@ -0,0 +1,773 @@
+\chapter{Vernacular commands}
+\label{Vernacular-commands}
+\label{Other-commands}
+
+\section{Displaying}
+
+\subsection{\tt Print {\qualid}.}\comindex{Print}
+This command displays on the screen informations about the declared or
+defined object referred by {\qualid}.
+
+\begin{ErrMsgs}
+\item {\qualid} \errindex{not a defined object}
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt Print Term {\qualid}.}
+\comindex{Print Term}\\ 
+This is a synonym to {\tt Print {\qualid}} when {\qualid} denotes a
+global constant. 
+
+\item {\tt About {\qualid}.}
+\label{About}
+\comindex{About}\\ 
+This displays various informations about the object denoted by {\qualid}:
+its kind (module, constant, assumption, inductive,
+constructor, abbreviation\ldots), long name, type, implicit
+arguments and argument scopes.
+
+%\item {\tt Print Proof {\qualid}.}\comindex{Print Proof}\\
+%In case \qualid\ denotes an opaque theorem defined in a section,
+%it is stored on a special unprintable form and displayed as 
+%{\tt <recipe>}. {\tt Print Proof} forces the printable form of \qualid\
+%to be computed and displays it.
+\end{Variants}
+
+\subsection{\tt Print All.}\comindex{Print All}
+This command displays informations about the current state of the
+environment, including sections and modules.
+
+\begin{Variants}
+\item {\tt Inspect \num.}\comindex{Inspect}\\
+This command displays the {\num} last objects of the current
+environment, including sections and modules.
+\item {\tt Print Section {\ident}.}\comindex{Print Section}\\
+should correspond to a currently open section, this command
+displays the objects defined since the beginning of this section.
+% Discontinued
+%% \item {\tt Print.}\comindex{Print}\\
+%% This command displays the axioms and variables declarations in the
+%% environment as well as the constants defined since the last variable
+%% was introduced.
+\end{Variants}
+
+\section{Requests to the environment}
+
+\subsection{\tt Check {\term}.}
+\label{Check}
+\comindex{Check}
+This command displays the type of {\term}. When called in proof mode, 
+the term is checked in the local context of the current subgoal.
+
+\subsection{\tt Eval {\rm\sl convtactic} in {\term}.}
+\comindex{Eval}
+
+This command performs the specified reduction on {\term}, and displays
+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).
+
+\SeeAlso section~\ref{Conversion-tactics}.
+
+\subsection{\tt Extraction \term.}
+\label{ExtractionTerm}
+\comindex{Extraction} 
+This command displays the extracted term from
+{\term}. The extraction is processed according to the distinction
+between {\Set} and {\Prop}; that is to say, between logical and
+computational content (see section \ref{Sorts}). The extracted term is
+displayed in Objective Caml syntax, where global identifiers are still
+displayed as in \Coq\ terms.
+
+\begin{Variants}
+\item \texttt{Recursive Extraction {\qualid$_1$} \ldots{} {\qualid$_n$}.}\\
+  Recursively extracts all the material needed for the extraction of 
+  globals {\qualid$_1$} \ldots{} {\qualid$_n$}.
+\end{Variants}
+
+\SeeAlso chapter~\ref{Extraction}.
+
+\subsection{\tt Opaque \qualid$_1$ \dots \qualid$_n$.}
+\comindex{Opaque}\label{Opaque} This command tells not to unfold the
+the constants {\qualid$_1$} \dots {\qualid$_n$} in tactics using
+$\delta$-conversion. Unfolding a constant is replacing it by its
+definition. {\tt Opaque} can only apply on constants originally
+defined as {\tt Transparent}.
+
+Constants defined by a proof ended by {\tt Qed} are automatically
+stamped as {\tt Opaque} and can no longer be considered as {\tt
+Transparent}. This is to keep with the usual mathematical practice of
+{\em proof irrelevance}: what matters in a mathematical development is
+the sequence of lemma statements, not their actual proofs. This
+distinguishes lemmas from the usual defined constants, whose actual
+values are of course relevant in general.
+
+\SeeAlso sections \ref{Conversion-tactics}, \ref{Automatizing},
+\ref{Theorem}
+
+\begin{ErrMsgs}
+\item \errindex{The reference \qualid\ was not found in the current
+environment}\\
+    There is no constant referred by {\qualid} in the environment.
+    Nevertheless, if you asked \texttt{Opaque foo bar}
+    and if \texttt{bar} does not exist, \texttt{foo} is set opaque.
+\end{ErrMsgs}
+
+\subsection{\tt Transparent \qualid$_1$ \dots \qualid$_n$.}
+\comindex{Transparent}\label{Transparent}
+This command is the converse of {\tt Opaque} and can only apply on constants originally defined as {\tt Transparent} to restore their initial behaviour after an {\tt Opaque} command.
+
+The constants automatically declared transparent are the ones defined by a proof ended by {\tt Defined}, or by a {\tt
+  Definition} or {\tt Local} with an explicit body.
+
+\Warning {\tt Transparent} and \texttt{Opaque} are not synchronous
+with the reset mechanism. If a constant was transparent at point A, if
+you set it opaque at point B and reset to point A, you return to state
+of point A with the difference that the constant is still opaque. This
+can cause changes in tactic scripts behaviour.
+
+At section or module closing, a constant recovers the status it got at
+the time of its definition.
+
+%TODO: expliquer le rapport avec les sections
+
+\begin{ErrMsgs}
+% \item \errindex{Can not set transparent.}\\
+%     It is a constant from a required module or a parameter.
+\item \errindex{The reference \qualid\ was not found in the current
+environment}\\
+    There is no constant referred by {\qualid} in the environment.
+\end{ErrMsgs}
+
+\SeeAlso sections \ref{Conversion-tactics}, \ref{Automatizing},
+\ref{Theorem}
+
+\subsection{\tt Search {\qualid}.}\comindex{Search}
+This command displays the name and type of all theorems of the current
+context whose statement's conclusion has the form {\tt ({\qualid} t1 ..
+  tn)}.  This command is useful to remind the user of the name of
+library lemmas.
+\begin{ErrMsgs}
+\item \errindex{The reference \qualid\ was not found in the current
+environment}\\
+    There is no constant in the environment named \qualid.
+\end{ErrMsgs}
+
+\begin{Variants}
+\item
+{\tt Search {\qualid} inside {\module$_1$} \ldots{} {\module$_n$}.}
+
+This restricts the search to constructions defined in modules
+{\module$_1$} \ldots{} {\module$_n$}.
+
+\item {\tt Search {\qualid} outside {\module$_1$} \ldots{} {\module$_n$}.}
+
+This restricts the search to constructions not defined in modules
+{\module$_1$} \ldots{} {\module$_n$}.
+
+\begin{ErrMsgs}
+\item \errindex{Module/section \module{} not found}
+No module \module{} has been required (see section~\ref{Require}).
+\end{ErrMsgs}
+
+\end{Variants}
+
+\subsection{\tt SearchAbout {\qualid}.}\comindex{SearchAbout}
+This command displays the name and type of all objects (theorems,
+axioms, etc) of the current context whose statement contains \qualid.
+This command is useful to remind the user of the name of library
+lemmas.
+
+\begin{ErrMsgs}
+\item \errindex{The reference \qualid\ was not found in the current
+environment}\\
+    There is no constant in the environment named \qualid.
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{}
+].}\\
+\noindent where {\textrm{\textsl{qualid-or-string}}} is a {\qualid} or
+a {\str}.
+
+This extension of {\tt SearchAbout} searches for all objects whose
+statement mentions all of {\qualid} of the list and whose name
+contains all {\str} of the list.
+
+\Example
+
+\begin{coq_example}
+Require Import ZArith.
+SearchAbout [ Zmult Zplus "distr" ].
+\end{coq_example}
+
+\item
+\begin{tabular}[t]{@{}l}
+  {\tt SearchAbout {\term} inside {\module$_1$} \ldots{} {\module$_n$}.} \\
+  {\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{} ]
+    inside {\module$_1$} \ldots{} {\module$_n$}.}
+\end{tabular}
+
+This restricts the search to constructions defined in modules
+{\module$_1$} \ldots{} {\module$_n$}.
+
+\item
+\begin{tabular}[t]{@{}l}
+  {\tt SearchAbout {\term} outside {\module$_1$}...{\module$_n$}.} \\
+  {\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{} ]
+     outside {\module$_1$}...{\module$_n$}.}
+\end{tabular}
+
+This restricts the search to constructions not defined in modules
+{\module$_1$} \ldots{} {\module$_n$}.
+
+\end{Variants}
+
+\subsection{\tt SearchPattern {\term}.}\comindex{SearchPattern}
+
+This command displays the name and type of all theorems of the current
+context whose statement's conclusion matches the expression {\term}
+where holes in the latter are denoted by ``{\texttt \_}''.
+
+\begin{coq_example}
+Require Import Arith.
+SearchPattern (_ + _ = _ + _).
+\end{coq_example}
+
+Patterns need not be linear: you can express that the same expression
+must occur in two places by using pattern variables `{\texttt
+?{\ident}}''.
+
+\begin{coq_example}
+Require Import Arith.
+SearchPattern (?X1 + _ = _ + ?X1).
+\end{coq_example}
+
+\begin{Variants}
+\item {\tt SearchPattern {\term} inside
+{\module$_1$} \ldots{} {\module$_n$}.}\comindex{SearchPattern \ldots{} inside
+\ldots{}}
+
+This restricts the search to constructions defined in modules
+{\module$_1$} \ldots{} {\module$_n$}.
+
+\item {\tt SearchPattern {\term} outside {\module$_1$} \ldots{} {\module$_n$}.}\comindex{SearchPattern \ldots{} outside \ldots{}}
+
+This restricts the search to constructions not defined in modules
+{\module$_1$} \ldots{} {\module$_n$}.
+
+\end{Variants}
+
+\subsection{\tt SearchRewrite {\term}.}\comindex{SearchRewrite}
+
+This command displays the name and type of all theorems of the current
+context whose statement's conclusion is an equality of which one side matches
+the expression {\term =}. Holes in {\term} are denoted by ``{\texttt \_}''.
+
+\begin{coq_example}
+Require Import Arith.
+SearchRewrite (_ + _ + _).
+\end{coq_example}
+
+\begin{Variants}
+\item {\tt SearchRewrite {\term} inside
+{\module$_1$} \ldots{} {\module$_n$}.}
+
+This restricts the search to constructions defined in modules
+{\module$_1$} \ldots{} {\module$_n$}.
+
+\item {\tt SearchRewrite {\term} outside {\module$_1$} \ldots{} {\module$_n$}.}
+
+This restricts the search to constructions not defined in modules
+{\module$_1$} \ldots{} {\module$_n$}.
+
+\end{Variants}
+
+% \subsection{\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
+% \>1.\>$A=B\mx{ if }A\stackrel{\bt{}\io{}}{\lra{}}B$\\
+% \>2.\>$\sa{}x:A.B=\sa{}y:A.B[x\la{}y]\mx{ if }y\not\in{}FV(\sa{}x:A.B)$\\
+% \>3.\>$\Pi{}x:A.B=\Pi{}y:A.B[x\la{}y]\mx{ if }y\not\in{}FV(\Pi{}x:A.B)$\\
+% \>4.\>$\sa{}x:A.B=\sa{}x:B.A\mx{ if }x\not\in{}FV(A,B)$\\
+% \>5.\>$\sa{}x:(\sa{}y:A.B).C=\sa{}x:A.\sa{}y:B[y\la{}x].C[x\la{}(x,y)]$\\
+% \>6.\>$\Pi{}x:(\sa{}y:A.B).C=\Pi{}x:A.\Pi{}y:B[y\la{}x].C[x\la{}(x,y)]$\\
+% \>7.\>$\Pi{}x:A.\sa{}y:B.C=\sa{}y:(\Pi{}x:A.B).(\Pi{}x:A.C[y\la{}(y\sm{}x)]$\\
+% \>8.\>$\sa{}x:A.unit=A$\\
+% \>9.\>$\sa{}x:unit.A=A[x\la{}tt]$\\
+% \>10.\>$\Pi{}x:A.unit=unit$\\
+% \>11.\>$\Pi{}x:unit.A=A[x\la{}tt]$
+% \end{tabbing}
+
+% For more informations about the exact working of this command, see
+% \cite{Del97}.
+
+\subsection{\tt Locate {\qualid}.}\comindex{Locate}
+\label{Locate}
+This command displays the full name of the qualified identifier {\qualid}
+and consequently the \Coq\ module in which it is defined.
+
+\begin{coq_eval}
+(*************** The last line should produce **************************)
+(*********** Error: I.Dont.Exist not a defined object ******************)
+\end{coq_eval}
+\begin{coq_eval}
+Set Printing Depth 50.
+\end{coq_eval}
+\begin{coq_example}
+Locate nat.
+Locate Datatypes.O.
+Locate Init.Datatypes.O.
+Locate Coq.Init.Datatypes.O.
+Locate I.Dont.Exist.
+\end{coq_example}
+
+\SeeAlso Section \ref{LocateSymbol}
+
+\section{Loading files}
+
+\Coq\ offers the possibility of loading different
+parts of a whole development stored in separate files. Their contents
+will be loaded as if they were entered from the keyboard. This means
+that the loaded files are ASCII files containing sequences of commands
+for \Coq's toplevel. This kind of file is called a {\em script} for
+\Coq\index{Script file}. The standard (and default) extension of
+\Coq's script files is {\tt .v}.
+
+\subsection{\tt Load {\ident}.}
+\comindex{Load}\label{Load}
+This command loads the file named {\ident}{\tt .v}, searching
+successively in each of the directories specified in the {\em
+  loadpath}. (see section \ref{loadpath})
+
+\begin{Variants}
+\item {\tt Load {\str}.}\label{Load-str}\\
+  Loads the file denoted by the string {\str}, where {\str} is any
+  complete filename. Then the \verb.~. and {\tt ..}
+  abbreviations are allowed as well as shell variables. If no
+  extension is specified, \Coq\ will use the default extension {\tt
+    .v}
+\item {\tt Load Verbose {\ident}.}, 
+  {\tt Load Verbose {\str}}\\
+  \comindex{Load Verbose}
+  Display, while loading, the answers of \Coq\ to each command
+  (including tactics) contained in the loaded file
+  \SeeAlso section \ref{Begin-Silent}
+\end{Variants}
+
+\begin{ErrMsgs}
+\item \errindex{Can't find file {\ident} on loadpath}
+\end{ErrMsgs}
+
+\section{Compiled files}\label{compiled}\index{Compiled files}
+
+This feature allows to build files for a quick loading. When loaded,
+the commands contained in a compiled file will not be {\em replayed}.
+In particular, proofs will not be replayed. This avoids a useless
+waste of time.
+
+\Rem A module containing an opened section cannot be compiled. 
+
+% \subsection{\tt Compile Module {\ident}.}
+% \index{Modules}
+% \comindex{Compile Module}
+% \index{.vo files}
+% This command loads the file
+% {\ident}{\tt .v} and plays the script it contains. Declarations,
+% definitions and proofs it contains are {\em "packaged"} in a compiled
+% form: the {\em module} named {\ident}.
+% A file {\ident}{\tt .vo} is then created.
+% The file {\ident}{\tt .v} is searched according to the
+% current loadpath.
+% The {\ident}{\tt .vo} is then written in the directory where
+% {\ident}{\tt .v} was found.
+
+% \begin{Variants}
+% \item \texttt{Compile Module {\ident} {\str}.}\\ 
+%   Uses the file {\str}{\tt .v} or {\str} if the previous one does not
+%   exist to build the module {\ident}. In this case, {\str} is any
+%   string giving a filename in the UNIX sense (see section
+%   \ref{Load-str}). 
+%   \Warning The given filename can not contain other caracters than
+%   the caracters of \Coq's identifiers : letters or digits or the
+%   underscore symbol ``\_''.
+
+% \item \texttt{Compile Module Specification {\ident}.}\\
+%   \comindex{Compile Module Specification}
+%   Builds a specification module: only the types of terms are stored
+%   in the module. The bodies (the proofs) are {\em not} written
+%   in the module. In that case, the file created is {\ident}{\tt .vi}.
+%   This is only useful when proof terms take too much place in memory
+%   and are not necessary.
+  
+% \item \texttt{Compile Verbose Module {\ident}.}\\ 
+%   \comindex{Compile Verbose Module}
+%   Verbose version of Compile: shows the contents of the file being
+%   compiled.
+% \end{Variants}
+
+% These different variants can be combined.
+
+
+% \begin{ErrMsgs}
+% \item \texttt{You cannot open a module when there are things other than}\\
+%   \texttt{Modules and Imports in the context.}\\ 
+%   The only commands allowed before a {Compile Module} command are {\tt
+%     Require},\\
+%   {\tt Read Module} and {\tt Import}. Actually, The normal way to
+%   compile modules is by the {\tt coqc} command (see chapter
+%   \ref{Addoc-coqc}).
+% \end{ErrMsgs}
+
+% \SeeAlso sections \ref{Opaque}, \ref{loadpath}, chapter
+% \ref{Addoc-coqc}
+
+%\subsection{\tt Import {\qualid}.}\comindex{Import}
+%\label{Import}
+
+%%%%%%%%%%%%
+% Import and Export described in RefMan-mod.tex
+% the minor difference (to avoid multiple Exporting of libraries) in
+% the treatment of normal modules and libraries by Export omitted
+
+
+\subsection{\tt Require {\dirpath}.}
+\label{Require}
+\comindex{Require}
+
+This command looks in the loadpath for a file containing module
+{\dirpath}, then loads and opens (imports) its contents.
+More precisely, if {\dirpath} splits into a library dirpath {\dirpath'} and a module name {\textsl{ident}}, then the file {\ident}{\tt .vo} is searched in a physical path mapped to the logical path {\dirpath'}.
+
+TODO: effect on the name table.
+
+% The implementation file ({\ident}{\tt .vo}) is searched first,
+% then the specification file ({\ident}{\tt .vi}) in case of failure.
+If the module required has already been loaded, \Coq\ 
+simply opens it (as {\tt Import {\dirpath}} would do it).
+%If the module required is already loaded and open, \Coq\ 
+%displays the following warning: {\tt {\ident} already imported}.
+
+If a module {\it A} contains a command {\tt Require} {\it B} then the
+command {\tt Require} {\it A} loads the module {\it B} but does not
+open it (See the {\tt Require Export} variant below).
+
+\begin{Variants}
+\item {\tt Require Export {\qualid}.}\\
+  \comindex{Require Export}
+  This command acts as {\tt Require} {\qualid}.  But if a module {\it
+    A} contains a command {\tt Require Export} {\it B}, then the
+  command {\tt Require} {\it A} opens the module {\it B} as if the
+  user would have typed {\tt Require}{\it B}.
+% \item {\tt Require $[$ Implementation $|$ Specification $]$ {\qualid}.}\\
+%   \comindex{Require Implementation}
+%   \comindex{Require Specification}
+%   Is the same as {\tt Require}, but specifying explicitly the
+%   implementation ({\tt.vo} file) or the specification ({\tt.vi}
+%   file).
+
+% Redundant ?
+% \item {\tt Require {\qualid} {\str}.}\\ 
+%   Specifies the file to load as being {\str} but containing module
+%  {\qualid}. 
+% The opened module is still {\ident} and therefore must have been loaded.
+\item {\tt Require {\qualid} {\str}.}\\ 
+  Specifies the file to load as being {\str} but containing module
+  {\qualid} which is then opened.
+\end{Variants}
+
+These different variants can be combined.
+
+\begin{ErrMsgs}
+
+\item \errindex{Cannot load {\ident}: no physical path bound to {\dirpath}}
+
+\item \errindex{Can't find module toto on loadpath}
+
+  The command did not find the file {\tt toto.vo}. Either {\tt
+    toto.v} exists but is not compiled or {\tt toto.vo} is in a directory
+  which is not in your {\tt LoadPath} (see section \ref{loadpath}).
+
+\item \errindex{Bad magic number}
+
+  \index{Bad-magic-number@{\tt Bad Magic Number}}
+  The file {\tt{\ident}.vo} was found but either it is not a \Coq\
+  compiled module, or it was compiled with an older and incompatible
+  version of \Coq.
+\end{ErrMsgs}
+
+\SeeAlso chapter \ref{Addoc-coqc}
+
+\subsection{\tt Print Modules.}
+\comindex{Print Modules}
+This command shows the currently loaded and currently opened
+(imported) modules.
+
+\subsection{\tt Declare ML Module {\str$_1$} .. {\str$_n$}.}
+\comindex{Declare ML Module}
+This commands loads the Objective Caml compiled files {\str$_1$} \dots
+{\str$_n$} (dynamic link). It is mainly used to load tactics
+dynamically.
+% (see chapter \ref{WritingTactics}).
+ The files are
+searched into the current Objective Caml loadpath (see the command {\tt
+Add ML Path} in the section \ref{loadpath}).  Loading of Objective Caml
+files is only possible under the bytecode version of {\tt coqtop}
+(i.e. {\tt coqtop} called with options {\tt -byte}, see chapter 
+\ref{Addoc-coqc}).
+
+\begin{ErrMsgs}
+\item \errindex{File not found on loadpath : \str}
+\item \errindex{Loading of ML object file forbidden in a native Coq}
+\end{ErrMsgs}
+
+\subsection{\tt Print ML Modules.}\comindex{Print ML Modules}
+This print the name of all \ocaml{} modules loaded with \texttt{Declare
+  ML Module}. To know from where these module were loaded, the user
+should use the command \texttt{Locate File} (see page \pageref{Locate File})
+
+\section{Loadpath}
+\label{loadpath}\index{Loadpath}
+
+There are currently two loadpaths in \Coq. A loadpath where seeking
+{\Coq} files (extensions {\tt .v} or {\tt .vo} or {\tt .vi}) and one where
+seeking Objective Caml files. The default loadpath contains the
+directory ``\texttt{.}'' denoting the current directory and mapped to the empty logical path (see section \ref{LongNames}).
+
+\subsection{\tt Pwd.}\comindex{Pwd}\label{Pwd}
+This command displays the current working directory.
+
+\subsection{\tt Cd {\str}.}\comindex{Cd}
+This command changes the current directory according to {\str} 
+which can be any valid path.
+
+\begin{Variants}
+\item {\tt Cd.}\\
+  Is equivalent to {\tt Pwd.}
+\end{Variants}
+
+\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} becomes accessible
+through logical name ``{\dirpath}{\tt{.M}}''. 
+
+\Rem {\tt Add LoadPath} also adds {\str} to the current ML loadpath.
+
+\begin{Variants}
+\item {\tt Add LoadPath {\str}.}\\
+Performs as {\tt Add LoadPath {\str} as {\dirpath}} but for the empty directory path.
+\end{Variants}
+
+\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} while any subdirectory {\textsl{pdir}} is mapped to logical directory {\dirpath}{\tt{.pdir}} and so on.
+
+\Rem {\tt Add Rec LoadPath} also recursively adds {\str} to the current ML loadpath.
+
+\begin{Variants}
+\item {\tt Add Rec LoadPath {\str}.}\\
+Works as {\tt Add Rec LoadPath {\str} as {\dirpath}} but for the empty logical directory path.
+\end{Variants}
+
+\subsection{\tt Remove LoadPath {\str}.}\comindex{Remove LoadPath}
+This command removes the path {\str} from the current \Coq\ loadpath.
+
+\subsection{\tt Print LoadPath.}\comindex{Print LoadPath}
+This command displays the current \Coq\ loadpath.
+
+\subsection{\tt Add ML Path {\str}.}\comindex{Add ML Path}
+This command adds the path {\str} to the current Objective Caml loadpath (see
+the command {\tt Declare ML Module} in the section \ref{compiled}).
+
+\Rem This command is implied by {\tt Add LoadPath {\str} as {\dirpath}}.
+
+\subsection{\tt Add Rec ML Path {\str}.}\comindex{Add Rec ML Path}
+This command adds the directory {\str} and all its subdirectories 
+to the current Objective Caml loadpath (see
+the command {\tt Declare ML Module} in the section \ref{compiled}).
+
+\Rem This command is implied by {\tt Add Rec LoadPath {\str} as {\dirpath}}.
+
+\subsection{\tt Print ML Path {\str}.}\comindex{Print ML Path}
+This command displays the current Objective Caml loadpath.
+This command makes sense only under the bytecode version of {\tt
+coqtop}, i.e. using option {\tt -byte} (see the
+command {\tt Declare ML Module} in the section
+\ref{compiled}).
+
+\subsection{\tt Locate File {\str}.}\comindex{Locate
+  File}\label{Locate File}
+This command displays the location of file {\str} in the current loadpath.
+Typically, {\str} is a \texttt{.cmo} or \texttt{.vo} or \texttt{.v} file.
+
+\subsection{\tt Locate Library {\dirpath}.}
+\comindex{Locate Library}
+This command gives the status of the \Coq\ module {\dirpath}. It tells if the
+module is loaded and if not searches in the load path for a module
+of logical name {\dirpath}.
+
+\section{States and Reset}
+
+\subsection{\tt Reset \ident.}
+\comindex{Reset}
+This command removes all the objects in the environment since \ident\ 
+was introduced, including \ident. \ident\ may be the name of a defined
+or declared object as well as the name of a section.  One cannot reset
+over the name of a module or of an object inside a module.
+
+\begin{ErrMsgs}
+\item \ident: \errindex{no such entry}
+\end{ErrMsgs}
+
+\subsection{\tt Back.}
+\comindex{Back}
+
+This commands undoes all the effects of the last vernacular
+command. This does not include commands that only access to the
+environment like those described in the previous sections of this
+chapter (for instance {\tt Require} and {\tt Load} can be undone, but
+not {\tt Check} and {\tt Locate}). Commands read from a vernacular
+file are considered as a single command.
+
+\begin{Variants}
+\item {\tt Back $n$} \\
+  Undoes $n$ vernacular commands.
+\end{Variants}
+
+\begin{ErrMsgs}
+\item \errindex{Reached begin of command history} \\
+  Happens when there is vernacular command to undo.
+\end{ErrMsgs}
+
+\subsection{\tt Restore State \str.}
+\comindex{Restore State}
+  Restores the state contained in the file \str.
+
+\begin{Variants}
+\item {\tt Restore State \ident}\\
+ Equivalent to {\tt Restore State "}{\ident}{\tt .coq"}.
+\item {\tt Reset Initial.}\comindex{Reset Initial}\\ 
+  Goes back to the initial state (like after the command {\tt coqtop},
+  when the interactive session began). This command is only available
+  interactively.
+\end{Variants}
+
+\subsection{\tt Write State \str.}
+\comindex{Write State}
+Writes the current state into a file \str{} for
+use in a further session. This file can be given as the {\tt
+  inputstate} argument of the commands {\tt coqtop} and {\tt coqc}.
+
+\begin{Variants}
+\item {\tt Write State \ident}\\
+ Equivalent to {\tt Write State "}{\ident}{\tt .coq"}.
+ The state is saved in the current directory (see \pageref{Pwd}).
+\end{Variants}
+
+\section{Quitting and debugging}
+
+\subsection{\tt Quit.}\comindex{Quit}
+This command permits to quit \Coq.
+
+\subsection{\tt Drop.}\comindex{Drop}\label{Drop}
+
+This is used mostly as a debug facility by \Coq's implementors
+and does not concern the casual user.
+This command permits to leave {\Coq} temporarily and enter the
+Objective Caml toplevel. The Objective Caml command:
+
+\begin{flushleft}
+\begin{verbatim}
+#use "include";;
+\end{verbatim}
+\end{flushleft}
+
+\noindent add the right loadpaths and loads some toplevel printers for
+all abstract types of \Coq - section\_path, identfifiers, terms, judgements,
+\dots. You can also use the file \texttt{base\_include} instead,
+that loads only the pretty-printers for section\_paths and
+identifiers.
+% See section \ref{test-and-debug} more information on the
+% usage of the toplevel.
+You can return back to \Coq{} with the command: 
+
+\begin{flushleft}
+\begin{verbatim}
+go();;
+\end{verbatim}
+\end{flushleft}
+
+\begin{Warnings}
+\item It only works with the bytecode version of {\Coq} (i.e. {\tt coqtop} called with option {\tt -byte}, see page \pageref{binary-images}).
+\item You must have compiled {\Coq} from the source package and set the
+  environment variable \texttt{COQTOP} to the root of your copy of the sources (see section \ref{EnvVariables}).
+\end{Warnings}
+
+\subsection{\tt Time \textrm{\textsl{command}}.}\comindex{Time}
+\label{time}
+This command executes the vernac command \textrm{\textsl{command}}
+and display the time needed to execute it.
+
+\section{Controlling display}
+
+\subsection{\tt Set Silent.}
+\comindex{Begin Silent}
+\label{Begin-Silent}
+\index{Silent mode}
+This command turns off the normal displaying.
+
+\subsection{\tt Unset Silent.}\comindex{End Silent}
+This command turns the normal display on.
+
+\subsection{\tt Set Printing Width {\integer}.}\comindex{Set Printing Width}
+This command sets which left-aligned part of the width of the screen
+is used for display. 
+
+\subsection{\tt Unset Printing Width.}\comindex{Unset Printing Width}
+This command resets the width of the screen used for display to its
+default value (which is 78 at the time of writing this documentation).
+
+\subsection{\tt Test Printing Width.}\comindex{Test Printing Width}
+This command displays the current screen width used for display.
+
+\subsection{\tt Set Printing Depth {\integer}.}\comindex{Set Printing Depth}
+This command sets the nesting depth of the formatter used for
+pretty-printing. Beyond this depth, display of subterms is replaced by
+dots. 
+
+\subsection{\tt Unset Printing Depth.}\comindex{Unset Printing Depth}
+This command resets the nesting depth of the formatter used for
+pretty-printing to its default value (at the
+time of writing this documentation, the default value is 50).
+
+\subsection{\tt Test Printing Depth.}\comindex{Test Printing Depth}
+This command displays the current nesting depth used for display.
+
+%\subsection{\tt Explain ...}
+%Not yet documented.
+
+%\subsection{\tt Go ...}
+%Not yet documented.
+
+%\subsection{\tt Abstraction ...}
+%Not yet documented.
+
+% $Id: RefMan-oth.tex 8606 2006-02-23 13:58:10Z herbelin $ 
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: 
-- 
cgit v1.2.3

