From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 14 Oct 2010 17:51:11 +0200
Subject: Imported Upstream version 8.3

---
 doc/refman/RefMan-oth.tex | 1181 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 1181 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..920e86de
--- /dev/null
+++ b/doc/refman/RefMan-oth.tex
@@ -0,0 +1,1181 @@
+\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: 
-- 
cgit v1.2.3

