diff options
Diffstat (limited to 'doc/refman/RefMan-oth.tex')
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 773 |
1 files changed, 773 insertions, 0 deletions
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: |