diff options
Diffstat (limited to 'doc/refman/RefMan-oth.tex')
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 1181 |
1 files changed, 0 insertions, 1181 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex deleted file mode 100644 index 920e86de..00000000 --- a/doc/refman/RefMan-oth.tex +++ /dev/null @@ -1,1181 +0,0 @@ -\chapter[Vernacular commands]{Vernacular commands\label{Vernacular-commands} -\label{Other-commands}} - -\section{Displaying} - -\subsection[\tt Print {\qualid}.]{\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. It does not print the body of -definitions or proofs. - -%\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.]{\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{Options and Flags} -\subsection[\tt Set {\rm\sl option} {\rm\sl value}.]{\tt Set {\rm\sl option} {\rm\sl value}.\comindex{Set}} -This command sets {\rm\sl option} to {\rm\sl value}. The original value of -{\rm\sl option} is restored when the current module ends. - -\begin{Variants} -\item {\tt Set {\rm\sl flag}.}\\ -This command switches {\rm\sl flag} on. The original state of -{\rm\sl flag} is restored when the current module ends. -\item {\tt Local Set {\rm\sl option} {\rm\sl value}.\comindex{Local Set}} -This command sets {\rm\sl option} to {\rm\sl value}. The original value of -{\rm\sl option} is restored when the current \emph{section} ends. -\item {\tt Local Set {\rm\sl flag}.}\\ -This command switches {\rm\sl flag} on. The original state of -{\rm\sl flag} is restored when the current \emph{section} ends. -\item {\tt Global Set {\rm\sl option} {\rm\sl value}.\comindex{Global Set}} -This command sets {\rm\sl option} to {\rm\sl value}. The original value of -{\rm\sl option} is \emph{not} restored at the end of the module. Additionally, -if set in a file, {\rm\sl option} is set to {\rm\sl value} when the file is -{\tt Require}-d. -\item {\tt Global Set {\rm\sl flag}.}\\ -This command switches {\rm\sl flag} on. The original state of -{\rm\sl flag} is \emph{not} restored at the end of the module. Additionally, -if set in a file, {\rm\sl flag} is switched on when the file is -{\tt Require}-d. -\end{Variants} - -\subsection[\tt Unset {\rm\sl flag}.]{\tt Unset {\rm\sl flag}.\comindex{Unset}} -This command switches {\rm\sl flag} off. The original state of {\rm\sl flag} -is restored when the current module ends. - -\begin{Variants} -\item {\tt Local Unset {\rm\sl flag}.\comindex{Local Unset}}\\ -This command switches {\rm\sl flag} off. The original state of {\rm\sl flag} -is restored when the current \emph{section} ends. -\item {\tt Global Unset {\rm\sl flag}.\comindex{Global Unset}}\\ -This command switches {\rm\sl flag} off. The original state of -{\rm\sl flag} is \emph{not} restored at the end of the module. Additionally, -if set in a file, {\rm\sl flag} is switched on when the file is -{\tt Require}-d. -\end{Variants} - -\subsection[\tt Test {\rm\sl option}.]{\tt Test {\rm\sl option}.\comindex{Test}} -This command prints the current value of {\rm\sl option}. - -\begin{Variants} -\item {\tt Test {\rm\sl flag}.}\\ -This command prints whether {\rm\sl flag} is on or off. -\end{Variants} - -\section{Requests to the environment} - -\subsection[\tt Check {\term}.]{\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}.]{\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 Compute {\term}.]{\tt Compute {\term}.\comindex{Compute}} - -This command performs a call-by-value evaluation of {\term} by using -the bytecode-based virtual machine. It is a shortcut for -{\tt Eval vm\_compute in {\term}}. - -\SeeAlso Section~\ref{Conversion-tactics}. - -\subsection[\tt Extraction \term.]{\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 Print Assumptions {\qualid}.]{\tt Print Assumptions {\qualid}.\comindex{Print Assumptions}} -\label{PrintAssumptions} - -This commands display all the assumptions (axioms, parameters and -variables) a theorem or definition depends on. Especially, it informs -on the assumptions with respect to which the validity of a theorem -relies. - -\begin{Variants} -\item \texttt{\tt Print Opaque Dependencies {\qualid}. - \comindex{Print Opaque Dependencies}}\\ - Displays the set of opaque constants {\qualid} relies on in addition - to the assumptions. -\end{Variants} - -\subsection[\tt Search {\term}.]{\tt Search {\term}.\comindex{Search}} -This command displays the name and type of all theorems of the current -context whose statement's conclusion has the form {\tt ({\term} t1 .. - tn)}. This command is useful to remind the user of the name of -library lemmas. - -\begin{coq_example} -Search le. -Search (@eq bool). -\end{coq_example} - -\begin{Variants} -\item -{\tt Search {\term} inside {\module$_1$} \ldots{} {\module$_n$}.} - -This restricts the search to constructions defined in modules -{\module$_1$} \ldots{} {\module$_n$}. - -\item {\tt Search {\term} 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}.]{\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} - -\newcommand{\termpatternorstr}{{\termpattern}\textrm{\textsl{-}}{\str}} - -\begin{Variants} -\item {\tt SearchAbout {\str}.} - -If {\str} is a valid identifier, this command displays the name and type -of all objects (theorems, axioms, etc) of the current context whose -name contains {\str}. If {\str} is a notation's string denoting some -reference {\qualid} (referred to by its main symbol as in \verb="+"= -or by its notation's string as in \verb="_ + _"= or \verb="_ 'U' _"=, see -Section~\ref{Notation}), the command works like {\tt SearchAbout -{\qualid}}. - -\item {\tt SearchAbout {\str}\%{\delimkey}.} - -The string {\str} must be a notation or the main symbol of a notation -which is then interpreted in the scope bound to the delimiting key -{\delimkey} (see Section~\ref{scopechange}). - -\item {\tt SearchAbout {\termpattern}.} - -This searches for all statements or types of definition that contains -a subterm that matches the pattern {\termpattern} (holes of the -pattern are either denoted by ``{\texttt \_}'' or -by ``{\texttt ?{\ident}}'' when non linear patterns are expected). - -\item {\tt SearchAbout [ \nelist{\zeroone{-}{\termpatternorstr}}{} -].}\\ - -\noindent where {\termpatternorstr} is a -{\termpattern} or a {\str}, or a {\str} followed by a scope -delimiting key {\tt \%{\delimkey}}. - -This generalization of {\tt SearchAbout} searches for all objects -whose statement or type contains a subterm matching {\termpattern} (or -{\qualid} if {\str} is the notation for a reference {\qualid}) and -whose name contains all {\str} of the request that correspond to valid -identifiers. If a {\termpattern} or a {\str} is prefixed by ``-'', the -search excludes the objects that mention that {\termpattern} or that -{\str}. - -\item -\begin{tabular}[t]{@{}l} - {\tt SearchAbout {\termpatternorstr} inside {\module$_1$} \ldots{} {\module$_n$}.} \\ - {\tt SearchAbout [ \nelist{{\termpatternorstr}}{} ] - 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 {\termpatternorstr} outside {\module$_1$}...{\module$_n$}.} \\ - {\tt SearchAbout [ \nelist{{\termpatternorstr}}{} ] - outside {\module$_1$}...{\module$_n$}.} -\end{tabular} - -This restricts the search to constructions not defined in modules -{\module$_1$} \ldots{} {\module$_n$}. - -\end{Variants} - -\examples - -\begin{coq_example*} -Require Import ZArith. -\end{coq_example*} -\begin{coq_example} -SearchAbout [ Zmult Zplus "distr" ]. -SearchAbout [ "+"%Z "*"%Z "distr" -positive -Prop]. -SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas. -\end{coq_example} - -\subsection[\tt SearchPattern {\termpattern}.]{\tt SearchPattern {\term}.\comindex{SearchPattern}} - -This command displays the name and type of all theorems of the current -context whose statement's conclusion or last hypothesis and conclusion -matches the expression {\term} where holes in the latter are denoted -by ``{\texttt \_}''. It is a variant of {\tt SearchAbout - {\termpattern}} that does not look for subterms but searches for -statements whose conclusion has exactly the expected form, or whose -statement finishes by the given series of hypothesis/conclusion. - -\begin{coq_example} -Require Import Arith. -SearchPattern (_ + _ = _ + _). -SearchPattern (nat -> bool). -SearchPattern (forall l : list _, _ l l). -\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$}.} - -This restricts the search to constructions defined in modules -{\module$_1$} \ldots{} {\module$_n$}. - -\item {\tt SearchPattern {\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 SearchRewrite {\term}.]{\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}.]{\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}.]{\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} - -\subsection{The {\sc Whelp} searching tool -\label{Whelp}} - -{\sc Whelp} is an experimental searching and browsing tool for the -whole {\Coq} library and the whole set of {\Coq} user contributions. -{\sc Whelp} requires a browser to work. {\sc Whelp} has been developed -at the University of Bologna as part of the HELM\footnote{Hypertextual -Electronic Library of Mathematics} and MoWGLI\footnote{Mathematics on -the Web, Get it by Logics and Interfaces} projects. It can be invoked -directly from the {\Coq} toplevel or from {\CoqIDE}, assuming a -graphical environment is also running. The browser to use can be -selected by setting the environment variable {\tt -COQREMOTEBROWSER}. If not explicitly set, it defaults to -\verb!firefox -remote \"OpenURL(%s,new-tab)\" || firefox %s &"! or -\verb!C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s!, depending on the -underlying operating system (in the command, the string \verb!%s! -serves as metavariable for the url to open). -The Whelp tool relies on a dedicated Whelp server and on another server -called Getter that retrieves formal documents. The default Whelp server name -can be obtained using the command {\tt Test Whelp Server} -\comindex{Test Whelp Server} and the default Getter can be obtained -using the command: {\tt Test Whelp Getter} \comindex{Test Whelp -Getter}. The Whelp server name can be changed using the command: - -\smallskip -\noindent {\tt Set Whelp Server {\str}}.\\ -where {\str} is a URL (e.g. {\tt http://mowgli.cs.unibo.it:58080}). -\comindex{Set Whelp Server} -\smallskip - -\noindent The Getter can be changed using the command: -\smallskip - -\noindent {\tt Set Whelp Getter {\str}}.\\ -where {\str} is a URL (e.g. {\tt http://mowgli.cs.unibo.it:58081}). -\comindex{Set Whelp Getter} - -\bigskip - -The {\sc Whelp} commands are: - -\subsubsection{\tt Whelp Locate "{\sl reg\_expr}". -\comindex{Whelp Locate}} - -This command opens a browser window and displays the result of seeking -for all names that match the regular expression {\sl reg\_expr} in the -{\Coq} library and user contributions. The regular expression can -contain the special operators are * and ? that respectively stand for -an arbitrary substring and for exactly one character. - -\variant {\tt Whelp Locate {\ident}.}\\ -This is equivalent to {\tt Whelp Locate "{\ident}"}. - -\subsubsection{\tt Whelp Match {\pattern}. -\comindex{Whelp Match}} - -This command opens a browser window and displays the result of seeking -for all statements that match the pattern {\pattern}. Holes in the -pattern are represented by the wildcard character ``\_''. - -\subsubsection[\tt Whelp Instance {\pattern}.]{\tt Whelp Instance {\pattern}.\comindex{Whelp Instance}} - -This command opens a browser window and displays the result of seeking -for all statements that are instances of the pattern {\pattern}. The -pattern is here assumed to be an universally quantified expression. - -\subsubsection[\tt Whelp Elim {\qualid}.]{\tt Whelp Elim {\qualid}.\comindex{Whelp Elim}} - -This command opens a browser window and displays the result of seeking -for all statements that have the ``form'' of an elimination scheme -over the type denoted by {\qualid}. - -\subsubsection[\tt Whelp Hint {\term}.]{\tt Whelp Hint {\term}.\comindex{Whelp Hint}} - -This command opens a browser window and displays the result of seeking -for all statements that can be instantiated so that to prove the -statement {\term}. - -\variant {\tt Whelp Hint.}\\ This is equivalent to {\tt Whelp Hint -{\sl goal}} where {\sl goal} is the current goal to prove. Notice that -{\Coq} does not send the local environment of definitions to the {\sc -Whelp} tool so that it only works on requests strictly based on, only, -definitions of the standard library and user contributions. - -\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}.]{\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]{Compiled files\label{compiled}\index{Compiled files}} - -This section describes the commands used to load compiled files (see -Chapter~\ref{Addoc-coqc} for documentation on how to compile a file). -A compiled file is a particular case of module called {\em library file}. - -%%%%%%%%%%%% -% 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 {\qualid}.]{\tt Require {\qualid}.\label{Require} -\comindex{Require}} - -This command looks in the loadpath for a file containing -module {\qualid} and adds the corresponding module to the environment -of {\Coq}. As library files have dependencies in other library files, -the command {\tt Require {\qualid}} recursively requires all library -files the module {\qualid} depends on and adds the corresponding modules to the -environment of {\Coq} too. {\Coq} assumes that the compiled files have -been produced by a valid {\Coq} compiler and their contents are then not -replayed nor rechecked. - -To locate the file in the file system, {\qualid} is decomposed under -the form {\dirpath}{\tt .}{\textsl{ident}} and the file {\ident}{\tt -.vo} is searched in the physical directory of the file system that is -mapped in {\Coq} loadpath to the logical path {\dirpath} (see -Section~\ref{loadpath}). The mapping between physical directories and -logical names at the time of requiring the file must be consistent -with the mapping used to compile the file. - -\begin{Variants} -\item {\tt Require Import {\qualid}.} \comindex{Require} - - This loads and declares the module {\qualid} and its dependencies - then imports the contents of {\qualid} as described in - Section~\ref{Import}. - - It does not import the modules on which {\qualid} depends unless - these modules were itself required in module {\qualid} using {\tt - Require Export}, as described below, or recursively required through - a sequence of {\tt Require Export}. - - If the module required has already been loaded, {\tt Require Import - {\qualid}} simply imports it, as {\tt Import {\qualid}} would. - -\item {\tt Require Export {\qualid}.} - \comindex{Require Export} - - This command acts as {\tt Require Import} {\qualid}, but if a - further module, say {\it A}, contains a command {\tt Require - Export} {\it B}, then the command {\tt Require Import} {\it A} - also imports the module {\it B}. - -\item {\tt Require \zeroone{Import {\sl |} Export} {\qualid}$_1$ \ldots {\qualid}$_n$.} - - This loads the modules {\qualid}$_1$, \ldots, {\qualid}$_n$ and - their recursive dependencies. If {\tt Import} or {\tt Export} is - given, it also imports {\qualid}$_1$, \ldots, {\qualid}$_n$ and all - the recursive dependencies that were marked or transitively marked - as {\tt Export}. - -\item {\tt Require \zeroone{Import {\sl |} Export} {\str}.} - - This shortcuts the resolution of the qualified name into a library - file name by directly requiring the module to be found in file - {\str}.vo. -\end{Variants} - -\begin{ErrMsgs} - -\item \errindex{Cannot load {\qualid}: no physical path bound to {\dirpath}} - -\item \errindex{Cannot find library foo in loadpath} - - The command did not find the file {\tt foo.vo}. Either {\tt - foo.v} exists but is not compiled or {\tt foo.vo} is in a directory - which is not in your {\tt LoadPath} (see Section~\ref{loadpath}). - -\item \errindex{Compiled library {\ident}.vo makes inconsistent assumptions over library {\qualid}} - - The command tried to load library file {\ident}.vo that depends on - some specific version of library {\qualid} which is not the one - already loaded in the current {\Coq} session. Probably {\ident}.v - was not properly recompiled with the last version of the file - containing module {\qualid}. - -\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. - -\item \errindex{The file {\ident}.vo contains library {\dirpath} and not - library {\dirpath'}} - - The library file {\dirpath'} is indirectly required by the {\tt - Require} command but it is bound in the current loadpath to the file - {\ident}.vo which was bound to a different library name {\dirpath} - at the time it was compiled. - -\end{ErrMsgs} - -\SeeAlso Chapter~\ref{Addoc-coqc} - -\subsection[\tt Print Libraries.]{\tt Print Libraries.\comindex{Print Libraries}} - -This command displays the list of library files loaded in the current -{\Coq} session. For each of these libraries, it also tells if it is -imported. - -\subsection[\tt Declare ML Module {\str$_1$} .. {\str$_n$}.]{\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}), or when Coq has been compiled with a version of -Objective Caml that supports native {\tt Dynlink} ($\ge$ 3.11). - -\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.]{\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 Section~\ref{Locate File}) - -\section[Loadpath]{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.]{\tt Pwd.\comindex{Pwd}\label{Pwd}} -This command displays the current working directory. - -\subsection[\tt Cd {\str}.]{\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}.]{\tt Add LoadPath {\str} as {\dirpath}.\comindex{Add LoadPath}\label{AddLoadPath}} - -This command adds the physical directory {\str} to the current {\Coq} -loadpath and maps it to the logical directory {\dirpath}, which means -that every file \textrm{\textsl{dirname}}/\textrm{\textsl{basename.v}} -physically lying in subdirectory {\str}/\textrm{\textsl{dirname}} -becomes accessible in {\Coq} through absolute logical name -{\dirpath}{\tt .}\textrm{\textsl{dirname}}{\tt -.}\textrm{\textsl{basename}}. - -\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}.]{\tt Add Rec LoadPath {\str} as {\dirpath}.\comindex{Add Rec LoadPath}\label{AddRecLoadPath}} -This command adds the physical directory {\str} and all its subdirectories to -the current \Coq\ loadpath. The top directory {\str} is mapped to the -logical directory {\dirpath} and any subdirectory {\textsl{pdir}} of it is -mapped to logical name {\dirpath}{\tt .}\textsl{pdir} and -recursively. Subdirectories corresponding to invalid {\Coq} -identifiers are skipped, and, by convention, subdirectories named {\tt -CVS} or {\tt \_darcs} are skipped too. - -Otherwise, said, {\tt Add Rec LoadPath {\str} as {\dirpath}} behaves -as {\tt Add LoadPath {\str} as {\dirpath}} excepts that files lying in -validly named subdirectories of {\str} need not be qualified to be -found. - -In case of files with identical base name, files lying in most recently -declared {\dirpath} are found first and explicit qualification is -required to refer to the other files of same base name. - -If several files with identical base name are present in different -subdirectories of a recursive loadpath declared via a single instance of -{\tt Add Rec LoadPath}, which of these files is found first is -system-dependent and explicit qualification is recommended. - -\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}.]{\tt Remove LoadPath {\str}.\comindex{Remove LoadPath}} -This command removes the path {\str} from the current \Coq\ loadpath. - -\subsection[\tt Print LoadPath.]{\tt Print LoadPath.\comindex{Print LoadPath}} -This command displays the current \Coq\ loadpath. - -\begin{Variants} -\item {\tt Print LoadPath {\dirpath}.}\\ -Works as {\tt Print LoadPath} but displays only the paths that extend the {\dirpath} prefix. -\end{Variants} - -\subsection[\tt Add ML Path {\str}.]{\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}.]{\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}.]{\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}.]{\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}.]{\tt Locate Library {\dirpath}.\comindex{Locate Library}\label{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.]{\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.]{\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 Backtrack $\num_1$ $\num_2$ $\num_3$.]{\tt Backtrack $\num_1$ $\num_2$ $\num_3$.\comindex{Backtrack}} - -This command is dedicated for the use in graphical interfaces. It -allows to backtrack to a particular \emph{global} state, i.e. -typically a state corresponding to a previous line in a script. A -global state includes declaration environment but also proof -environment (see Chapter~\ref{Proof-handling}). The three numbers -$\num_1$, $\num_2$ and $\num_3$ represent the following: -\begin{itemize} -\item $\num_3$: Number of \texttt{Abort} to perform, i.e. the number - of currently opened nested proofs that must be canceled (see - Chapter~\ref{Proof-handling}). -\item $\num_2$: \emph{Proof state number} to unbury once aborts have - been done. Coq will compute the number of \texttt{Undo} to perform - (see Chapter~\ref{Proof-handling}). -\item $\num_1$: Environment state number to unbury, Coq will compute - the number of \texttt{Back} to perform. -\end{itemize} - - -\subsubsection{How to get state numbers?} -\label{sec:statenums} - - -Notice that when in \texttt{-emacs} mode, \Coq\ displays the current -proof and environment state numbers in the prompt. More precisely the -prompt in \texttt{-emacs} mode is the following: - -\verb!<prompt>! \emph{$id_i$} \verb!<! $\num_1$ -\verb!|! $id_1$\verb!|!$id_2$\verb!|!\dots\verb!|!$id_n$ -\verb!|! $\num_2$ \verb!< </prompt>! - -Where: - -\begin{itemize} -\item \emph{$id_i$} is the name of the current proof (if there is - one, otherwise \texttt{Coq} is displayed, see -Chapter~\ref{Proof-handling}). -\item $\num_1$ is the environment state number after the last - command. -\item $\num_2$ is the proof state number after the last - command. -\item $id_1$ $id_2$ {\dots} $id_n$ are the currently opened proof names - (order not significant). -\end{itemize} - -It is then possible to compute the \texttt{Backtrack} command to -unbury the state corresponding to a particular prompt. For example, -suppose the current prompt is: - -\verb!<! goal4 \verb!<! 35 -\verb!|!goal1\verb!|!goal4\verb!|!goal3\verb!|!goal2\verb!|! -\verb!|!8 \verb!< </prompt>! - -and we want to backtrack to a state labeled by: - -\verb!<! goal2 \verb!<! 32 -\verb!|!goal1\verb!|!goal2 -\verb!|!12 \verb!< </prompt>! - -We have to perform \verb!Backtrack 32 12 2! , i.e. perform 2 -\texttt{Abort}s (to cancel goal4 and goal3), then rewind proof until -state 12 and finally go back to environment state 32. Notice that this -supposes that proofs are nested in a regular way (no \texttt{Resume} or -\texttt{Suspend} commands). - -\begin{Variants} -\item {\tt BackTo n}. \comindex{BackTo}\\ - Is a more basic form of \texttt{Backtrack} where only the first - argument (global environment number) is given, no \texttt{abort} and - no \texttt{Undo} is performed. -\end{Variants} - -\subsection[\tt Restore State \str.]{\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.]{\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 Section~\ref{Pwd}). -\end{Variants} - -\section{Quitting and debugging} - -\subsection[\tt Quit.]{\tt Quit.\comindex{Quit}} -This command permits to quit \Coq. - -\subsection[\tt Drop.]{\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, identifiers, terms, judgments, -\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 the contents of Section~\ref{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}}.]{\tt Time \textrm{\textsl{command}}.\comindex{Time} -\label{time}} -This command executes the vernacular command \textrm{\textsl{command}} -and display the time needed to execute it. - - -\subsection[\tt Timeout \textrm{\textsl{int}} \textrm{\textsl{command}}.]{\tt Timeout \textrm{\textsl{int}} \textrm{\textsl{command}}.\comindex{Timeout} -\label{timeout}} - -This command executes the vernacular command \textrm{\textsl{command}}. If -the command has not terminated after the time specified by the integer -(time expressed in seconds), then it is interrupted and an error message -is displayed. - -\section{Controlling display} - -\subsection[\tt Set Silent.]{\tt Set Silent.\comindex{Set Silent} -\label{Begin-Silent} -\index{Silent mode}} -This command turns off the normal displaying. - -\subsection[\tt Unset Silent.]{\tt Unset Silent.\comindex{Unset Silent}} -This command turns the normal display on. - -\subsection[\tt Set Printing Width {\integer}.]{\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.]{\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.]{\tt Test Printing Width.\comindex{Test Printing Width}} -This command displays the current screen width used for display. - -\subsection[\tt Set Printing Depth {\integer}.]{\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.]{\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.]{\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. - -\section{Controlling the reduction strategies and the conversion algorithm} -\label{Controlling reduction strategy} - -{\Coq} provides reduction strategies that the tactics can invoke and -two different algorithms to check the convertibility of types. -The first conversion algorithm lazily -compares applicative terms while the other is a brute-force but efficient -algorithm that first normalizes the terms before comparing them. The -second algorithm is based on a bytecode representation of terms -similar to the bytecode representation used in the ZINC virtual -machine~\cite{Leroy90}. It is specially useful for intensive -computation of algebraic values, such as numbers, and for reflexion-based -tactics. The commands to fine-tune the reduction strategies and the -lazy conversion algorithm are described first. - -\subsection[\tt Opaque \qualid$_1$ {\dots} \qualid$_n$.]{\tt Opaque \qualid$_1$ {\dots} \qualid$_n$.\comindex{Opaque}\label{Opaque}} -This command has an effect on unfoldable constants, i.e. -on constants defined by {\tt Definition} or {\tt Let} (with an explicit -body), or by a command assimilated to a definition such as {\tt -Fixpoint}, {\tt Program Definition}, etc, or by a proof ended by {\tt -Defined}. The command tells not to unfold -the constants {\qualid$_1$} {\dots} {\qualid$_n$} in tactics using -$\delta$-conversion (unfolding a constant is replacing it by its -definition). - -{\tt Opaque} has also on effect on the conversion algorithm of {\Coq}, -telling to delay the unfolding of a constant as later as possible in -case {\Coq} has to check the conversion (see Section~\ref{conv-rules}) -of two distinct applied constants. - -The scope of {\tt Opaque} is limited to the current section, or -current file, unless the variant {\tt Global Opaque \qualid$_1$ {\dots} -\qualid$_n$} is used. - -\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$.]{\tt Transparent \qualid$_1$ {\dots} \qualid$_n$.\comindex{Transparent}\label{Transparent}} -This command is the converse of {\tt Opaque} and it applies on -unfoldable constants to restore their unfoldability after an {\tt -Opaque} command. - -Note in particular that constants defined by a proof ended by {\tt -Qed} are not unfoldable and {\tt Transparent} has no effect on -them. 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. - -The scope of {\tt Transparent} is limited to the current section, or -current file, unless the variant {\tt Global Transparent \qualid$_1$ -\dots \qualid$_n$} is used. - -\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 Strategy {\it level} [ \qualid$_1$ {\dots} \qualid$_n$ - ].\comindex{Strategy}\comindex{Local Strategy}\label{Strategy}} -This command generalizes the behavior of {\tt Opaque} and {\tt - Transparent} commands. It is used to fine-tune the strategy for -unfolding constants, both at the tactic level and at the kernel -level. This command associates a level to \qualid$_1$ {\dots} -\qualid$_n$. Whenever two expressions with two distinct head -constants are compared (for instance, this comparison can be triggered -by a type cast), the one with lower level is expanded first. In case -of a tie, the second one (appearing in the cast type) is expanded. - -Levels can be one of the following (higher to lower): -\begin{description} -\item[opaque]: level of opaque constants. They cannot be expanded by - tactics (behaves like $+\infty$, see next item). -\item[\num]: levels indexed by an integer. Level $0$ corresponds - to the default behavior, which corresponds to transparent - constants. This level can also be referred to as {\bf transparent}. - Negative levels correspond to constants to be expanded before normal - transparent constants, while positive levels correspond to constants - to be expanded after normal transparent constants. -\item[expand]: level of constants that should be expanded first - (behaves like $-\infty$) -\end{description} - -These directives survive section and module closure, unless the -command is prefixed by {\tt Local}. In the latter case, the behavior -regarding sections and modules is the same as for the {\tt - Transparent} and {\tt Opaque} commands. - -\subsection{\tt Declare Reduction \ident\ := {\rm\sl convtactic}.} - -This command allows to give a short name to a reduction expression, -for instance {\tt lazy beta delta [foo bar]}. This short name can -then be used in {\tt Eval \ident\ in ...} or {\tt eval} directives. -This command accepts the {\tt Local} modifier, for discarding -this reduction name at the end of the file or module. For the moment -the name cannot be qualified. In particular declaring the same name -in several modules or in several functor applications will be refused -if these declarations are not local. The name \ident\ cannot be used -directly as an Ltac tactic, but nothing prevent the user to also -perform a {\tt Ltac \ident\ := {\rm\sl convtactic}}. - -\SeeAlso sections \ref{Conversion-tactics} - -\subsection{\tt Set Virtual Machine -\label{SetVirtualMachine} -\comindex{Set Virtual Machine}} - -This activates the bytecode-based conversion algorithm. - -\subsection{\tt Unset Virtual Machine -\comindex{Unset Virtual Machine}} - -This deactivates the bytecode-based conversion algorithm. - -\subsection{\tt Test Virtual Machine -\comindex{Test Virtual Machine}} - -This tells if the bytecode-based conversion algorithm is -activated. The default behavior is to have the bytecode-based -conversion algorithm deactivated. - -\SeeAlso sections~\ref{vmcompute} and~\ref{vmoption}. - -\section{Controlling the locality of commands} - -\subsection{{\tt Local}, {\tt Global} -\comindex{Local} -\comindex{Global} -} - -Some commands support a {\tt Local} or {\tt Global} prefix modifier to -control the scope of their effect. There are four kinds of commands: - -\begin{itemize} -\item Commands whose default is to extend their effect both outside the - section and the module or library file they occur in. - - For these commands, the {\tt Local} modifier limits the effect of - the command to the current section or module it occurs in. - - As an example, the {\tt Coercion} (see Section~\ref{Coercions}) - and {\tt Strategy} (see Section~\ref{Strategy}) - commands belong to this category. - -\item Commands whose default behavior is to stop their effect at the - end of the section they occur in but to extent their effect outside - the module or library file they occur in. - - For these commands, the {\tt Local} modifier limits the effect of - the command to the current module if the command does not occur in a - section and the {\tt Global} modifier extends the effect outside the - current sections and current module if the command occurs in a - section. - - As an example, the {\tt Implicit Arguments} (see - Section~\ref{Implicit Arguments}), {\tt Ltac} (see - Chapter~\ref{TacticLanguage}) or {\tt Notation} (see - Section~\ref{Notation}) commands belong to this category. - - Notice that a subclass of these commands do not support extension of - their scope outside sections at all and the {\tt Global} is not - applicable to them. - -\item Commands whose default behavior is to stop their effect at the - end of the section or module they occur in. - - For these commands, the {\tt Global} modifier extends their effect - outside the sections and modules they occurs in. - - The {\tt Transparent} and {\tt Opaque} (see - Section~\ref{Controlling reduction strategy}) commands belong to - this category. - -\item Commands whose default behavior is to extend their effect - outside sections but not outside modules when they occur in a - section and to extend their effect outside the module or library - file they occur in when no section contains them. - - For these commands, the {\tt Local} modifier limits the effect to - the current section or module while the {\tt Global} modifier extends - the effect outside the module even when the command occurs in a section. - - The {\tt Set} and {\tt Unset} commands belong to this category. -\end{itemize} - - -% $Id: RefMan-oth.tex 13454 2010-09-23 17:00:29Z aspiwack $ - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: |