From 8fbe7741c3e374a2a15adf68a59824f4190b7e20 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Mar 2018 09:44:15 +0100
Subject: [Sphinx] Move chapter 6 to new infrastructure

---
 doc/refman/RefMan-oth.tex | 1224 ---------------------------------------------
 1 file changed, 1224 deletions(-)
 delete 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
deleted file mode 100644
index bef31d3fa5..0000000000
--- a/doc/refman/RefMan-oth.tex
+++ /dev/null
@@ -1,1224 +0,0 @@
-\chapter[Vernacular commands]{Vernacular commands\label{Vernacular-commands}
-\label{Other-commands}}
-%HEVEA\cutname{vernacular.html}
-
-\section{Displaying}
-
-\subsection[\tt Print {\qualid}.]{\tt Print {\qualid}.\comindex{Print}}
-This command displays on the screen information about the declared or
-defined object referred by {\qualid}.
-
-\begin{ErrMsgs}
-\item {\qualid} \errindex{not a defined object}
-\item \errindex{Universe instance should have length} $n$.
-\item \errindex{This object does not support universe names.}
-\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 information 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 {\qualid}@\{names\}.}\\
-This locally renames the polymorphic universes of {\qualid}.
-An underscore means the raw universe is printed.
-This form can be used with {\tt Print Term} and {\tt About}.
-
-%\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 information 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{Flags, Options and Tables}
-
-{\Coq} configurability is based on flags (e.g. {\tt Set Printing All} in
-Section~\ref{SetPrintingAll}), options (e.g. {\tt Set Printing Width
-  {\integer}} in Section~\ref{SetPrintingWidth}), or tables (e.g. {\tt
-  Add Printing Record {\ident}}, in Section~\ref{AddPrintingLet}). The
-names of flags, options and tables are made of non-empty sequences of
-identifiers (conventionally with capital initial letter). The general
-commands handling flags, options and tables are given below.
-
-\subsection[\tt Set {\rm\sl flag}.]{\tt Set {\rm\sl flag}.\comindex{Set}}
-This command switches {\rm\sl flag} on. The original state of
-{\rm\sl flag} is restored when the current module ends.
-
-\begin{Variants}
-\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 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 off when the file is
-{\tt Require}-d.
-\end{Variants}
-
-\subsection[\tt Test {\rm\sl flag}.]{\tt Test {\rm\sl flag}.\comindex{Test}}
-This command prints whether {\rm\sl flag} is on or off.
-
-\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 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 at the end of the module.
-\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.
-\end{Variants}
-
-\subsection[\tt Unset {\rm\sl option}.]{\tt Unset {\rm\sl option}.\comindex{Unset}}
-This command resets {\rm\sl option} to its default value.
-
-\begin{Variants}
-\item {\tt Local Unset {\rm\sl option}.\comindex{Local Unset}}\\
-This command resets {\rm\sl option} to its default value. The original state of {\rm\sl option}
-is restored when the current \emph{section} ends.
-\item {\tt Global Unset {\rm\sl option}.\comindex{Global Unset}}\\
-This command resets {\rm\sl option} to its default value.  The original state of
-{\rm\sl option} is \emph{not} restored at the end of the module. Additionally,
-if unset in a file, {\rm\sl option} is reset to its default value 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}.
-
-\subsection{Tables}
-The general commands for tables are {\tt Add {\rm\sf table} {\rm\sl
-    value}}, {\tt Remove {\rm\sf table} {\rm\sl value}}, {\tt Test
-    {\rm\sf table}}, {\tt Test {\rm\sf table} for {\rm\sl value}} and
-  {\tt Print Table {\rm\sf table}}.
-
-\subsection[\tt Print Options.]{\tt Print Options.\comindex{Print Options}}
-This command lists all available flags, options and tables.
-
-\begin{Variants}
-\item {\tt Print Tables}.\comindex{Print Tables}\\
-This is a synonymous of {\tt Print Options.}
-\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.
-
-\begin{Variants}
-\item {\tt selector: Check {\term}}.\\
-specifies on which subgoal to perform typing (see
-  Section~\ref{tactic-syntax}).
-\end{Variants}
-
-
-\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 {\ocaml} syntax, where global identifiers are still
-displayed as in \Coq\ terms.
-
-\begin{Variants}
-\item \texttt{Recursive Extraction} {\qualid$_1$} \ldots{} {\qualid$_n$}{\tt .}\\
-  Recursively extracts all the material needed for the extraction of 
-  global {\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.
-\item \texttt{\tt Print Transparent Dependencies {\qualid}.
-  \comindex{Print Transparent Dependencies}}\\
-  Displays the set of transparent constants {\qualid} relies on in addition
-  to the assumptions.
-\item \texttt{\tt Print All Dependencies {\qualid}.
-  \comindex{Print All Dependencies}}\\
-  Displays all assumptions and constants {\qualid} relies on.
-\end{Variants}
-
-\subsection[\tt Search {\qualid}.]{\tt Search {\qualid}.\comindex{Search}}
-This command displays the name and type of all objects (hypothesis of
-the current goal, 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 Search {\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 Search
-{\qualid}}.
-
-\item {\tt Search {\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 Search {\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 Search \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 Search} 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
-  {\tt Search} \nelist{{\termpatternorstr}}{}
-    {\tt inside} {\module$_1$} \ldots{} {\module$_n$}{\tt .}
-
-This restricts the search to constructions defined in modules
-{\module$_1$} \ldots{} {\module$_n$}.
-
-\item
-  {\tt Search \nelist{{\termpatternorstr}}{}
-     outside {\module$_1$}...{\module$_n$}.}
-
-This restricts the search to constructions not defined in modules
-{\module$_1$} \ldots{} {\module$_n$}.
-
-\item {\tt selector: Search \nelist{\zeroone{-}{\termpatternorstr}}{}.}
-
-  This specifies the goal on which to search hypothesis (see
-  Section~\ref{tactic-syntax}). By default the 1st goal is searched.
-  This variant can be combined with other variants presented here.
-\end{Variants}
-
-\examples
-
-\begin{coq_example*}
-Require Import ZArith.
-\end{coq_example*}
-\begin{coq_example}
-Search Z.mul Z.add "distr".
-Search "+"%Z "*"%Z "distr" -positive -Prop.
-Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
-\end{coq_example}
-
-\Warning \comindex{SearchAbout} Up to {\Coq} version 8.4, {\tt Search}
-had the behavior of current {\tt SearchHead} and the behavior of
-current {\tt Search} was obtained with command {\tt SearchAbout}. For
-compatibility, the deprecated name {\tt SearchAbout} can still be used
-as a synonym of {\tt Search}. For compatibility, the list of objects to
-search when using {\tt SearchAbout} may also be enclosed by optional
-{\tt [ ]} delimiters.
-
-\subsection[\tt SearchHead {\term}.]{\tt SearchHead {\term}.\comindex{SearchHead}}
-This command displays the name and type of all hypothesis of the
-current goal (if any) and 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_eval}
-Reset Initial.
-\end{coq_eval}
-
-\begin{coq_example}
-SearchHead le.
-SearchHead (@eq bool).
-\end{coq_example}
-
-\begin{Variants}
-\item
-{\tt SearchHead} {\term} {\tt inside} {\module$_1$} \ldots{} {\module$_n$}{\tt .}
-
-This restricts the search to constructions defined in modules
-{\module$_1$} \ldots{} {\module$_n$}.
-
-\item {\tt SearchHead} {\term} {\tt outside} {\module$_1$} \ldots{} {\module$_n$}{\tt .}
-
-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}
-
-\item {\tt selector: SearchHead {\term}.}
-
-  This specifies the goal on which to search hypothesis (see
-  Section~\ref{tactic-syntax}). By default the 1st goal is searched.
-  This variant can be combined with other variants presented here.
-
-\end{Variants}
-
-\Warning Up to {\Coq} version 8.4, {\tt SearchHead} was named {\tt Search}.
-
-\subsection[\tt SearchPattern {\termpattern}.]{\tt SearchPattern {\term}.\comindex{SearchPattern}}
-
-This command displays the name and type of all hypothesis of the
-current goal (if any) and 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 Search
-  {\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.
-\end{coq_example*}
-\begin{coq_example}
-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}
-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$}.
-
-\item {\tt selector: SearchPattern {\term}.}
-
-  This specifies the goal on which to search hypothesis (see
-  Section~\ref{tactic-syntax}). By default the 1st goal is searched.
-  This variant can be combined with other variants presented here.
-
-\end{Variants}
-
-\subsection[\tt SearchRewrite {\term}.]{\tt SearchRewrite {\term}.\comindex{SearchRewrite}}
-
-This command displays the name and type of all hypothesis of the
-current goal (if any) and 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$}.
-
-\item {\tt selector: SearchRewrite {\term}.}
-
-  This specifies the goal on which to search hypothesis (see
-  Section~\ref{tactic-syntax}). By default the 1st goal is searched.
-  This variant can be combined with other variants presented here.
-
-\end{Variants}
-
-\subsubsection{Nota Bene:}
-For the {\tt Search}, {\tt SearchHead}, {\tt SearchPattern} and
-{\tt SearchRewrite} queries, it is possible to globally filter
-the search results via the command
-{\tt Add Search Blacklist "substring1"}.
-A lemma whose fully-qualified name contains any of the declared substrings
-will be removed from the search results.
-The default blacklisted substrings are {\tt 
-  "\_subproof" "Private\_"}. The command {\tt Remove Search Blacklist
-  ...} allows expunging this blacklist.
-
-% \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 objects whose name is a prefix of the
-qualified identifier {\qualid}, and consequently the \Coq\ module in which they
-are defined. It searches for objects from the different qualified name spaces of
-{\Coq}: terms, modules, Ltac, etc.
-
-\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}
-
-\begin{Variants}
-\item {\tt Locate Term {\qualid}.}\comindex{Locate Term}\\
-  As {\tt Locate} but restricted to terms.
-
-\item {\tt Locate Module {\qualid}.}
-  As {\tt Locate} but restricted to modules.
-
-\item {\tt Locate Ltac {\qualid}.}\comindex{Locate Ltac}\\
-  As {\tt Locate} but restricted to tactics.
-\end{Variants}
-
-
-\SeeAlso Section \ref{LocateSymbol}
-
-\section{Loading files}
-
-\Coq\ offers the possibility of loading different
-parts of a whole development stored in separate files. Their contents
-will be loaded as if they were entered from the keyboard. This means
-that the loaded files are ASCII files containing sequences of commands
-for \Coq's toplevel. This kind of file is called a {\em script} for
-\Coq\index{Script file}. The standard (and default) extension of
-\Coq's script files is {\tt .v}.
-
-\subsection[\tt Load {\ident}.]{\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})
-
-Files loaded this way cannot leave proofs open, and neither the {\tt
-  Load} command can be use inside a proof.
-
-\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}
-\item \errindex{Load is not supported inside proofs}
-\item \errindex{Files processed by Load cannot leave open proofs}
-\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. If several files match, one of them
-is picked in an unspecified fashion.
-
-\begin{Variants}
-\item {\tt Require Import {\qualid}.} \comindex{Require Import}
-
-  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${\tt .}
-
-  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 From {\dirpath} Require {\qualid}.}
-  \comindex{From Require}
-
-  This command acts as {\tt Require}, but picks any library whose absolute name
-  is of the form {\tt{\dirpath}.{\dirpath'}.{\qualid}} for some {\dirpath'}.
-  This is useful to ensure that the {\qualid} library comes from a given
-  package by making explicit its absolute root.
-
-\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.
-
-\item \errindex{Require is not allowed inside a module or a module type}
-
-  This command is not allowed inside a module or a module type being defined.
-  It is meant to describe a dependency between compilation units. Note however
-  that the commands {\tt Import} and {\tt Export} alone can be used inside
-  modules (see Section~\ref{Import}).
-
-\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 {\ocaml} compiled files {\str$_1$} {\ldots}
-{\str$_n$} (dynamic link). It is mainly used to load tactics
-dynamically.
-% (see Chapter~\ref{WritingTactics}).
- The files are
-searched into the current {\ocaml} loadpath (see the command {\tt
-Add ML Path} in the Section~\ref{loadpath}).  Loading of {\ocaml}
-files is only possible under the bytecode version of {\tt coqtop}
-(i.e. {\tt coqtop.byte}, see chapter 
-\ref{Addoc-coqc}), or when {\Coq} has been compiled with a version of
-{\ocaml} that supports native {\tt Dynlink} ($\ge$ 3.11).
-
-\begin{Variants}
-\item {\tt Local Declare ML Module {\str$_1$} .. {\str$_n$}.}\\
-  This variant is not exported to the modules that import the module
-  where they occur, even if outside a section.
-\end{Variants}
-
-\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}
-
-Loadpaths are preferably managed using {\Coq} command line options
-(see Section~\ref{loadpath}) but there remain vernacular commands to
-manage them for practical purposes. Such commands are only meant to be issued in
-the toplevel, and using them in source files is discouraged.
-
-\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 is equivalent to the command line option {\tt -Q {\str}
-  {\dirpath}}. It adds the physical directory {\str} to the current {\Coq}
-loadpath and maps it to the logical directory {\dirpath}.
-
-\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 is equivalent to the command line option {\tt -R {\str}
-  {\dirpath}}. It adds the physical directory {\str} and all its
-subdirectories to the current {\Coq} 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 {\ocaml} loadpath (see
-the command {\tt Declare ML Module} in the Section~\ref{compiled}).
-
-\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 {\ocaml} loadpath (see
-the command {\tt Declare ML Module} in the Section~\ref{compiled}).
-
-\subsection[\tt Print ML Path {\str}.]{\tt Print ML Path {\str}.\comindex{Print ML Path}}
-This command displays the current {\ocaml} loadpath.
-This command makes sense only under the bytecode version of {\tt
-coqtop}, i.e. {\tt coqtop.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{Backtracking}
-
-The backtracking commands described in this section can only be used
-interactively, they cannot be part of a vernacular file loaded via
-{\tt Load} or compiled by {\tt coqc}.
-
-\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}
-
-\begin{Variants}
- \item {\tt Reset Initial.}\comindex{Reset Initial}\\
-   Goes back to the initial state, just after the start of the
-   interactive session.
-\end{Variants}
-
-\subsection[\tt Back.]{\tt Back.\comindex{Back}}
-
-This commands undoes all the effects of the last vernacular
-command. Commands read from a vernacular file via a {\tt Load} are
-considered as a single command. Proof management commands
-are also handled by this command (see Chapter~\ref{Proof-handling}).
-For that, {\tt Back} may have to undo more than one command in order
-to reach a state where the proof management information is available.
-For instance, when the last command is a {\tt Qed}, the management
-information about the closed proof has been discarded. In this case,
-{\tt Back} will then undo all the proof steps up to the statement of
-this proof.
-
-\begin{Variants}
-\item {\tt Back $n$} \\
-  Undoes $n$ vernacular commands. As for {\tt Back}, some extra
-  commands may be undone in order to reach an adequate state.
-  For instance {\tt Back n} will not re-enter a closed proof,
-  but rather go just before that proof.
-\end{Variants}
-
-\begin{ErrMsgs}
-\item \errindex{Invalid backtrack} \\
-  The user wants to undo more commands than available in the history.
-\end{ErrMsgs}
-
-\subsection[\tt BackTo $\num$.]{\tt BackTo $\num$.\comindex{BackTo}}
-\label{sec:statenums}
-
-This command brings back the system to the state labeled $\num$,
-forgetting the effect of all commands executed after this state.
-The state label is an integer which grows after each successful command.
-It is displayed in the prompt when in \texttt{-emacs} mode.
-Just as {\tt Back} (see above), the {\tt BackTo} command now handles
-proof states. For that, it may have to undo some
-extra commands and end on a state $\num' \leq \num$ if necessary.
-
-\begin{Variants}
-\item {\tt Backtrack $\num_1$ $\num_2$ $\num_3$}.\comindex{Backtrack}\\
-  {\tt Backtrack} is a \emph{deprecated} form of {\tt BackTo} which
-  allows explicitly manipulating the proof environment. 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$: State label to reach, as for {\tt BackTo}.
-\end{itemize}
-\end{Variants}
-
-\begin{ErrMsgs}
-\item \errindex{Invalid backtrack} \\
-  The destination state label is unknown.
-\end{ErrMsgs}
-
-\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
-{\ocaml} toplevel. The {\ocaml} 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 Redirect "\textrm{\textsl{file}}" \textrm{\textsl{command}}.]{\tt Redirect "\textrm{\textsl{file}}" \textrm{\textsl{command}}.\comindex{Redirect}
-\label{redirect}}
-This command executes the vernacular command \textrm{\textsl{command}}, redirecting its output to ``\textrm{\textsl{file}}.out''.
-
-\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.
-
-\subsection[\tt Set Default Timeout \textrm{\textsl{int}}.]{\tt Set
-  Default Timeout \textrm{\textsl{int}}.\optindex{Default Timeout}}
-
-After using this command, all subsequent commands behave as if they
-were passed to a {\tt Timeout} command. Commands already starting by
-a {\tt Timeout} are unaffected.
-
-\subsection[\tt Unset Default Timeout.]{\tt Unset Default Timeout.\optindex{Default Timeout}}
-
-This command turns off the use of a default timeout.
-
-\subsection[\tt Test Default Timeout.]{\tt Test Default Timeout.\optindex{Default Timeout}}
-
-This command displays whether some default timeout has be set or not.
-
-\subsection[\tt Fail \textrm{\textsl{command-or-tactic}}.]{\tt Fail \textrm{\textsl{command-or-tactic}}.\comindex{Fail}\label{Fail}}
-
-For debugging {\Coq} scripts, sometimes it is desirable to know
-whether a command or a tactic fails. If the given command or tactic
-fails, the {\tt Fail} statement succeeds, without changing the proof
-state, and in interactive mode, {\Coq} prints a message confirming the failure.
-If the command or tactic succeeds, the statement is an error, and
-{\Coq} prints a message indicating that the failure did not occur.
-
-\section{Controlling display}
-
-\subsection[\tt Set Silent.]{\tt Set Silent.\optindex{Silent}
-\label{Begin-Silent}
-\index{Silent mode}}
-This command turns off the normal displaying.
-
-\subsection[\tt Unset Silent.]{\tt Unset Silent.\optindex{Silent}}
-This command turns the normal display on.
-
-\subsection[\tt Set Warnings ``(\nterm{w}$_1$,\ldots,%
-  \nterm{w}$_n$)''.]{{\tt Set Warnings ``(\nterm{w}$_1$,\ldots,%
-  \nterm{w}$_n$)''}.\optindex{Warnings}}
-\label{SetWarnings}
-This command configures the display of warnings. It is experimental, and
-expects, between quotes, a comma-separated list of warning names or
-categories. Adding~\texttt{-} in front of a warning or category disables it,
-adding~\texttt{+} makes it an error. It is possible to use the special
-categories \texttt{all} and \texttt{default}, the latter containing the warnings
-enabled by default. The flags are interpreted from left to right, so in case of
-an overlap, the flags on the right have higher priority, meaning that
-\texttt{A,-A} is equivalent to \texttt{-A}.
-
-\subsection[\tt Set Search Output Name Only.]{\tt Set Search Output Name Only.\optindex{Search Output Name Only}
-\label{Search-Output-Name-Only}
-\index{Search Output Name Only mode}}
-This command restricts the output of search commands to identifier names; turning it on causes invocations of {\tt Search}, {\tt SearchHead}, {\tt SearchPattern}, {\tt SearchRewrite} etc. to omit types from their output, printing only identifiers.
-
-\subsection[\tt Unset Search Output Name Only.]{\tt Unset Search Output Name Only.\optindex{Search Output Name Only}}
-This command turns type display in search results back on.
-
-\subsection[\tt Set Printing Width {\integer}.]{\tt Set Printing Width {\integer}.\optindex{Printing Width}}
-\label{SetPrintingWidth}
-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.\optindex{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.\optindex{Printing Width}}
-This command displays the current screen width used for display.
-
-\subsection[\tt Set Printing Depth {\integer}.]{\tt Set Printing Depth {\integer}.\optindex{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.\optindex{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.\optindex{Printing Depth}}
-This command displays the current nesting depth used for display.
-
-\subsection[\tt Unset Printing Compact Contexts.]{\tt Unset Printing Compact Contexts.\optindex{Printing Compact Contexts}}
-This command resets the displaying of goals contexts to non compact
-mode (default at the time of writing this documentation). Non compact
-means that consecutive variables of different types are printed on
-different lines.
-
-\subsection[\tt Set Printing Compact Contexts.]{\tt Set Printing Compact Contexts.\optindex{Printing Compact Contexts}}
-This command sets the displaying of goals contexts to compact mode.
-The printer tries to reduce the vertical size of goals contexts by
-putting several variables (even if of different types) on the same
-line provided it does not exceed the printing width (See {\tt Set
-  Printing Width} above).
-
-\subsection[\tt Test Printing Compact Contexts.]{\tt Test Printing Compact Contexts.\optindex{Printing Compact Contexts}}
-This command displays the current state of compaction of goal.
-
-
-\subsection[\tt Unset Printing Unfocused.]{\tt Unset Printing Unfocused.\optindex{Printing Unfocused}}
-This command resets the displaying of goals to focused goals only
-(default). Unfocused goals are created by focusing other goals with
-bullets(see~\ref{bullets}) or curly braces (see~\ref{curlybacket}).
-
-\subsection[\tt Set Printing Unfocused.]{\tt Set Printing Unfocused.\optindex{Printing Unfocused}}
-This command enables the displaying of unfocused goals. The goals are
-displayed after the focused ones and are distinguished by a separator.
-
-\subsection[\tt Test Printing Unfocused.]{\tt Test Printing Unfocused.\optindex{Printing Unfocused}}
-This command displays the current state of unfocused goals display.
-
-\subsection[\tt Set Printing Dependent Evars Line.]{\tt Set Printing Dependent Evars Line.\optindex{Printing Dependent Evars Line}}
-This command enables the printing of the ``{\tt (dependent evars: \ldots)}''
-line when {\tt -emacs} is passed.
-
-\subsection[\tt Unset Printing Dependent Evars Line.]{\tt Unset Printing Dependent Evars Line.\optindex{Printing Dependent Evars Line}}
-This command disables the printing of the ``{\tt (dependent evars: \ldots)}''
-line when {\tt -emacs} is passed.
-
-%\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 especially useful for intensive
-computation of algebraic values, such as numbers, and for reflection-based
-tactics. The commands to fine-tune the reduction strategies and the
-lazy conversion algorithm are described first.
-
-\subsection[{\tt Opaque} \qualid$_1$ {\ldots} \qualid$_n${\tt .}]{{\tt Opaque} \qualid$_1$ {\ldots} \qualid$_n${\tt .}\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$} {\ldots} {\qualid$_n$} in tactics using
-$\delta$-conversion (unfolding a constant is replacing it by its
-definition).
-
-{\tt Opaque} has also an effect on the conversion algorithm of {\Coq},
-telling it to delay the unfolding of a constant as much as possible when
-{\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$ {\ldots}
-\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$ {\ldots} \qualid$_n${\tt .}]{{\tt Transparent} \qualid$_1$ {\ldots} \qualid$_n${\tt .}\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$
-{\ldots} \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} {\tt [} \qualid$_1$ {\ldots} \qualid$_n$
-  {\tt ].}\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$ {\ldots}
-\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 Print Strategy} \qualid{\tt .}\comindex{Print Strategy}\label{PrintStrategy}}
-
-This command prints the strategy currently associated to \qualid{}. It fails if
-\qualid{} is not an unfoldable reference, that is, neither a variable nor a
-constant.
-
-\begin{ErrMsgs}
-\item The reference is not unfoldable.
-\end{ErrMsgs}
-
-\begin{Variants}
-\item {\tt Print Strategies}\comindex{Print Strategies}\\
-  Print all the currently non-transparent strategies.
-\end{Variants}
-
-\subsection{\tt Declare Reduction \ident\ := {\rm\sl convtactic}.}
-
-This command allows giving 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}
-
-\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}
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: 
-- 
cgit v1.2.3

