\chapter{Vernacular commands}
\label{Vernacular-commands}
\label{Other-commands}

\section{Displaying}

\subsection{\tt Print {\qualid}.}\comindex{Print}
This command displays on the screen informations about the declared or
defined object referred by {\qualid}.

\begin{ErrMsgs}
\item {\qualid} \errindex{not a defined object}
\end{ErrMsgs}

\begin{Variants}
\item {\tt Print Proof {\qualid}.}\comindex{Print Proof}\\
This is a synonym to {\tt Print {\qualid}} when {\qualid} denotes a global constant.
%In case \qualid\ denotes an opaque theorem defined in a section,
%it is stored on a special unprintable form and displayed as 
%{\tt <recipe>}. {\tt Print Proof} forces the printable form of \qualid\
%to be computed and displays it.
\end{Variants}

\subsection{\tt Print All.}\comindex{Print All}
This command displays informations about the current state of the
environment, including sections and modules.

\begin{Variants}
\item {\tt Inspect \num.}\comindex{Inspect}\\
This command displays the {\num} last objects of the current
environment, including sections and modules.
\item {\tt Print Section {\ident}.}\comindex{Print Section}\\
should correspond to a currently open section, this command
displays the objects defined since the beginning of this section.
\item {\tt Print.}\comindex{Print}\\
This command displays the axioms and variables declarations in the
environment as well as the constants defined since the last variable
was introduced.
\end{Variants}

\section{Requests to the environment}

\subsection{\tt Check {\term}.}
\label{Check}
\comindex{Check}
This command displays the type of {\term}. When called in proof mode, 
the term is checked in the local context of the current subgoal.

\begin{Variants}
\item \texttt{Check {\num} {\term}}\\
  Displays the type of {\term} in the context of the {\num}-th
  subgoal.
\end{Variants}

\subsection{\tt Eval {\rm\sl convtactic} in {\term}.}
\comindex{Eval}

This command performs the specified reduction on {\term}, and displays
the resulting term with its type. The term to be reduced may depend on
hypothesis introduced in the first subgoal (if a proof is in
progress).

\begin{Variants}
\item \texttt{Eval {\num} {\rm\sl convtactic} in {\term}.}\\
  Evaluates {\term} in the context of the {\num}-th subgoal.
\end{Variants}

\SeeAlso section~\ref{Conversion-tactics}.

\subsection{\tt Extraction \term.}
\label{ExtractionTerm}
\comindex{Extraction} 
This command displays the extracted term from
{\term}. The extraction is processed according to the distinction
between {\Set} and {\Prop}; that is to say, between logical and
computational content (see section \ref{Sorts}). The extracted term is
displayed in Objective Caml syntax, where global identifiers are still
displayed as in \Coq\ terms.

\begin{Variants}
\item \texttt{Recursive Extraction {\qualid$_1$} ... {\qualid$_n$}.}\\
  Recursively extracts all the material needed for the extraction of 
  globals {\qualid$_1$} ... {\qualid$_n$}.
\end{Variants}

\SeeAlso chapter~\ref{Extraction}.

\subsection{\tt Opaque \qualid$_1$ \dots \qualid$_n$.}
\comindex{Opaque}\label{Opaque} This command tells not to unfold the
the constants {\qualid$_1$} \dots {\qualid$_n$} in tactics using
$\delta$-conversion. Unfolding a constant is replacing it by its
definition. {\tt Opaque} can only apply on constants originally
defined as {\tt Transparent}.

Constants defined by a proof ended by {\tt Qed} are automatically
stamped as {\tt Opaque} and can no longer be considered as {\tt
Transparent}. This is to keep with the usual mathematical practice of
{\em proof irrelevance}: what matters in a mathematical development is
the sequence of lemma statements, not their actual proofs. This
distinguishes lemmas from the usual defined constants, whose actual
values are of course relevant in general.

\SeeAlso sections \ref{Conversion-tactics}, \ref{Automatizing},
\ref{Theorem}

\begin{ErrMsgs}
\item \errindex{The reference \qualid\ was not found in the current
environment}\\
    There is no constant referred by {\qualid} in the environment.
    Nevertheless, if you asked \texttt{Opaque foo bar}
    and if \texttt{bar} does not exist, \texttt{foo} is set opaque.
\end{ErrMsgs}

\subsection{\tt Transparent \qualid$_1$ \dots \qualid$_n$.}
\comindex{Transparent}\label{Transparent}
This command is the converse of {\tt Opaque} and can only apply on constants originally defined as {\tt Transparent} to restore their initial behaviour after an {\tt Opaque} command.

The constants automatically declared transparent are the ones defined by a proof ended by {\tt Defined}, or by a {\tt
  Definition} or {\tt Local} with an explicit body.

\Warning {\tt Transparent} and \texttt{Opaque} are not synchronous
with the reset mechanism. If a constant was transparent at point A, if
you set it opaque at point B and reset to point A, you return to state
of point A with the difference that the constant is still opaque. This
can cause changes in tactic scripts behaviour.

At section or module closing, a constant recovers the status it got at
the time of its definition.

%TODO: expliquer le rapport avec les sections

\begin{ErrMsgs}
% \item \errindex{Can not set transparent.}\\
%     It is a constant from a required module or a parameter.
\item \errindex{The reference \qualid\ was not found in the current
environment}\\
    There is no constant referred by {\qualid} in the environment.
\end{ErrMsgs}

\SeeAlso sections \ref{Conversion-tactics}, \ref{Automatizing},
\ref{Theorem}

\subsection{\tt Search {\qualid}.}\comindex{Search}
This command displays the name and type of all theorems of the current
context whose statement's conclusion has the form {\tt ({\qualid} t1 ..
  tn)}.  This command is useful to remind the user of the name of
library lemmas.
\begin{ErrMsgs}
\item \errindex{The reference \qualid\ was not found in the current
environment}\\
    There is no constant in the environment named
    \qualid.
\end{ErrMsgs}

\subsection{\tt SearchPattern {\term}.}\comindex{SearchPattern}

This command displays the name and type of all theorems of the current
context whose statement's conclusion matches the expression {\term}
where holes in the latter are denoted by ``{\texttt ?}''.

\begin{coq_example}
Require Arith.
SearchPattern (plus ? ?)=?.
\end{coq_example}

Patterns need not be linear: you can express that the same
expression must occur in two places by using indexed `{\texttt ?}''.

\begin{coq_example}
Require Arith.
SearchPattern (plus ?1 ?)=?1.
\end{coq_example}

\subsection{\tt SearchRewrite {\term}.}\comindex{SearchRewrite}

This command displays the name and type of all theorems of the current
context whose statement's conclusion is an equality of which one side matches
the expression {\term =}. Holes in {\term} are denoted by ``{\texttt ?}''.

\begin{coq_example}
Require Arith.
SearchRewrite (plus ? ?).
\end{coq_example}

\begin{Variants}
\item
{\tt Search {\qualid} inside
{\module$_1$}...{\module$_n$}.}\comindex{Search ... inside ...}\\
{\tt SearchPattern {\term} inside
{\module$_1$}...{\module$_n$}.}\comindex{SearchPattern ... inside
...}\\
{\tt SearchRewrite {\term} inside
{\module$_1$}...{\module$_n$}.}\comindex{SearchRewrite ... inside ...}

This restricts the search to constructions defined in modules {\module$_1$}...{\module$_n$}.

\item {\tt Search {\qualid} outside {\module$_1$}...{\module$_n$}.}\comindex{Search ... outside ...}\\
{\tt SearchPattern {\term} outside {\module$_1$}...{\module$_n$}.}\comindex{SearchPattern ... outside ...}\\
{\tt SearchRewrite {\term} outside {\module$_1$}...{\module$_n$}.}\comindex{SearchRewrite ... outside ...}

  This restricts the search to constructions not defined in modules
{\module$_1$}...{\module$_n$}.

\end{Variants}
\begin{ErrMsgs}
\item \errindex{Module/section \module{} not found}
No module \module{} has been required (see section~\ref{Require}).
\end{ErrMsgs}

% \subsection{\tt SearchIsos {\term}.}\comindex{SearchIsos}
% \label{searchisos}
% \texttt{SearchIsos} searches terms by their type modulo isomorphism.
% This command displays the full name of all constants, variables,
% inductive types, and inductive constructors of the current
% context whose type is isomorphic to {\term} modulo the contextual part of the
% following axiomatization (the mutual inductive types with one constructor,
% without implicit arguments, and for which projections exist, are regarded as a
% sequence of $\sa{}$):


% \begin{tabbing}
% \ \ \ \ \=11.\ \=\kill
% \>1.\>$A=B\mx{ if }A\stackrel{\bt{}\io{}}{\lra{}}B$\\
% \>2.\>$\sa{}x:A.B=\sa{}y:A.B[x\la{}y]\mx{ if }y\not\in{}FV(\sa{}x:A.B)$\\
% \>3.\>$\Pi{}x:A.B=\Pi{}y:A.B[x\la{}y]\mx{ if }y\not\in{}FV(\Pi{}x:A.B)$\\
% \>4.\>$\sa{}x:A.B=\sa{}x:B.A\mx{ if }x\not\in{}FV(A,B)$\\
% \>5.\>$\sa{}x:(\sa{}y:A.B).C=\sa{}x:A.\sa{}y:B[y\la{}x].C[x\la{}(x,y)]$\\
% \>6.\>$\Pi{}x:(\sa{}y:A.B).C=\Pi{}x:A.\Pi{}y:B[y\la{}x].C[x\la{}(x,y)]$\\
% \>7.\>$\Pi{}x:A.\sa{}y:B.C=\sa{}y:(\Pi{}x:A.B).(\Pi{}x:A.C[y\la{}(y\sm{}x)]$\\
% \>8.\>$\sa{}x:A.unit=A$\\
% \>9.\>$\sa{}x:unit.A=A[x\la{}tt]$\\
% \>10.\>$\Pi{}x:A.unit=unit$\\
% \>11.\>$\Pi{}x:unit.A=A[x\la{}tt]$
% \end{tabbing}

% For more informations about the exact working of this command, see
% \cite{Del97}.

\subsection{\tt Locate {\qualid}.}\comindex{Locate}
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 ******************)
(* Just to adjust the prompt: *) 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}

\section{Loading files}

\Coq\ offers the possibility of loading different
parts of a whole development stored in separate files. Their contents
will be loaded as if they were entered from the keyboard. This means
that the loaded files are ASCII files containing sequences of commands
for \Coq's toplevel. This kind of file is called a {\em script} for
\Coq\index{Script file}. The standard (and default) extension of
\Coq's script files is {\tt .v}.

\subsection{\tt Load {\ident}.}
\comindex{Load}\label{Load}
This command loads the file named {\ident}{\tt .v}, searching
successively in each of the directories specified in the {\em
  loadpath}. (see section \ref{loadpath})

\begin{Variants}
\item {\tt Load {\str}.}\label{Load-str}\\
  Loads the file denoted by the string {\str}, where {\str} is any
  complete filename. Then the \verb.~. and {\tt ..}
  abbreviations are allowed as well as shell variables. If no
  extension is specified, \Coq\ will use the default extension {\tt
    .v}
\item {\tt Load Verbose {\ident}.}, 
  {\tt Load Verbose {\str}}\\
  \comindex{Load Verbose}
  Display, while loading, the answers of \Coq\ to each command
  (including tactics) contained in the loaded file
  \SeeAlso section \ref{Begin-Silent}
\end{Variants}

\begin{ErrMsgs}
\item \errindex{Can't find file {\ident} on loadpath}
\end{ErrMsgs}

\section{Compiled files}\label{compiled}\index{Compiled files}

This feature allows to build files for a quick loading. When loaded,
the commands contained in a compiled file will not be {\em replayed}.
In particular, proofs will not be replayed. This avoids a useless
waste of time.

\Rem A module containing an opened section cannot be compiled. 

% \subsection{\tt Compile Module {\ident}.}
% \index{Modules}
% \comindex{Compile Module}
% \index{.vo files}
% This command loads the file
% {\ident}{\tt .v} and plays the script it contains. Declarations,
% definitions and proofs it contains are {\em "packaged"} in a compiled
% form: the {\em module} named {\ident}.
% A file {\ident}{\tt .vo} is then created.
% The file {\ident}{\tt .v} is searched according to the
% current loadpath.
% The {\ident}{\tt .vo} is then written in the directory where
% {\ident}{\tt .v} was found.

% \begin{Variants}
% \item \texttt{Compile Module {\ident} {\str}.}\\ 
%   Uses the file {\str}{\tt .v} or {\str} if the previous one does not
%   exist to build the module {\ident}. In this case, {\str} is any
%   string giving a filename in the UNIX sense (see section
%   \ref{Load-str}). 
%   \Warning The given filename can not contain other caracters than
%   the caracters of \Coq's identifiers : letters or digits or the
%   underscore symbol ``\_''.

% \item \texttt{Compile Module Specification {\ident}.}\\
%   \comindex{Compile Module Specification}
%   Builds a specification module: only the types of terms are stored
%   in the module. The bodies (the proofs) are {\em not} written
%   in the module. In that case, the file created is {\ident}{\tt .vi}.
%   This is only useful when proof terms take too much place in memory
%   and are not necessary.
  
% \item \texttt{Compile Verbose Module {\ident}.}\\ 
%   \comindex{Compile Verbose Module}
%   Verbose version of Compile: shows the contents of the file being
%   compiled.
% \end{Variants}

% These different variants can be combined.


% \begin{ErrMsgs}
% \item \texttt{You cannot open a module when there are things other than}\\
%   \texttt{Modules and Imports in the context.}\\ 
%   The only commands allowed before a {Compile Module} command are {\tt
%     Require},\\
%   {\tt Read Module} and {\tt Import}. Actually, The normal way to
%   compile modules is by the {\tt coqc} command (see chapter
%   \ref{Addoc-coqc}).
% \end{ErrMsgs}

% \SeeAlso sections \ref{Opaque}, \ref{loadpath}, chapter
% \ref{Addoc-coqc}

\subsection{\tt Read Module {\qualid}.}\comindex{Read Module}
This looks for a physical file \texttt{file.vo} mapped to logical name
{\qualid} in the current {\Coq} loadpath, then loads its contents but
does not open it: its contents remains accesible to the user only by
using names prefixed by the module name (i.e. {\qualid} or any other
qualified names denoting the same module).
%  The implementation file
% ({\ident}{\tt.vo}) is searched first, then the specification file
% ({\ident}{\tt.vi}) in case of failure.

\subsection{\tt Require {\dirpath}.}
\label{Require}
\comindex{Require}

This command looks in the loadpath for a file containing module
{\dirpath}, then loads and opens (imports) its contents.
More precisely, if {\dirpath} splits into a library dirpath {\dirpath'} and a module name {\textsl{ident}}, then the file {\ident}{\tt .vo} is searched in a physical path mapped to the logical path {\dirpath'}.

% The implementation file ({\ident}{\tt .vo}) is searched first,
% then the specification file ({\ident}{\tt .vi}) in case of failure.
If the module required has already been loaded, \Coq\ 
simply opens it (as {\tt Import {\dirpath}} would do it).
%If the module required is already loaded and open, \Coq\ 
%displays the following warning: {\tt {\ident} already imported}.

If a module {\it A} contains a command {\tt Require} {\it B} then the
command {\tt Require} {\it A} loads the module {\it B} but does not
open it (See the {\tt Require Export} variant below).

\begin{Variants}
\item {\tt Require Export {\qualid}.}\\
  \comindex{Require Export}
  This command acts as {\tt Require} {\qualid}.  But if a module {\it
    A} contains a command {\tt Require Export} {\it B}, then the
  command {\tt Require} {\it A} opens the module {\it B} as if the
  user would have typed {\tt Require}{\it B}.
% \item {\tt Require $[$ Implementation $|$ Specification $]$ {\qualid}.}\\
%   \comindex{Require Implementation}
%   \comindex{Require Specification}
%   Is the same as {\tt Require}, but specifying explicitly the
%   implementation ({\tt.vo} file) or the specification ({\tt.vi}
%   file).

% Redundant ?
% \item {\tt Require {\qualid} {\str}.}\\ 
%   Specifies the file to load as being {\str} but containing module
%  {\qualid}. 
% The opened module is still {\ident} and therefore must have been loaded.
\item {\tt Require {\qualid} {\str}.}\\ 
  Specifies the file to load as being {\str} but containing module
  {\qualid} which is then opened.
\end{Variants}

These different variants can be combined.

\begin{ErrMsgs}
\item \errindex{Cannot load {\ident}: no physical path bound to {\dirpath}}\\
\item \errindex{Can't find module toto on loadpath}\\
  The command did not find the file {\tt toto.vo}. Either {\tt
    toto.v} exists but is not compiled or {\tt toto.vo} is in a directory
  which is not in your {\tt LoadPath} (see section \ref{loadpath}).
\item \errindex{Bad magic number}\\
  \index{Bad-magic-number@{\tt Bad Magic Number}}
  The file {\tt{\ident}.vo} was found but either it is not a \Coq\
  compiled module, or it was compiled with an older and incompatible
  version of \Coq.
\end{ErrMsgs}

\SeeAlso chapter \ref{Addoc-coqc}

\subsection{\tt Print Modules.}
\comindex{Print Modules}
This command shows the currently loaded and currently opened
(imported) modules.

\subsection{\tt Declare ML Module {\str$_1$} .. {\str$_n$}.}
\comindex{Declare ML Module}
This commands loads the Objective Caml compiled files {\str$_1$} \dots
{\str$_n$} (dynamic link). It is mainly used to load tactics
dynamically.
% (see chapter \ref{WritingTactics}).
 The files are
searched into the current Objective Caml loadpath (see the command {\tt
Add ML Path} in the section \ref{loadpath}).  Loading of Objective Caml
files is only possible under the bytecode version of {\tt coqtop}
(i.e. {\tt coqtop} called with options {\tt -byte}, see chapter 
\ref{Addoc-coqc}).
\begin{ErrMsgs}
\item \errindex{File not found on loadpath : \str}
\item \errindex{Loading of ML object file forbidden in a native Coq}
\end{ErrMsgs}

\subsection{\tt Print ML Modules.}\comindex{Print ML Modules}
This print the name of all \ocaml{} modules loaded with \texttt{Declare
  ML Module}. To know from where these module were loaded, the user
should use the command \texttt{Locate File} (see page \pageref{Locate File})

\section{Loadpath}
\label{loadpath}\index{Loadpath}

There are currently two loadpaths in \Coq. A loadpath where seeking
{\Coq} files (extensions {\tt .v} or {\tt .vo} or {\tt .vi}) and one where
seeking Objective Caml files. The default loadpath contains the
directory ``\texttt{.}'' denoting the current directory and mapped to the empty logical path (see section \ref{LongNames}).

\subsection{\tt Pwd.}\comindex{Pwd}\label{Pwd}
This command displays the current working directory.

\subsection{\tt Cd {\str}.}\comindex{Cd}
This command changes the current directory according to {\str} 
which can be any valid path.

\begin{Variants}
\item {\tt Cd.}\\
  Is equivalent to {\tt Pwd.}
\end{Variants}

\subsection{\tt Add LoadPath {\str} as {\dirpath}.}
\comindex{Add LoadPath}\label{AddLoadPath}

This command adds the path {\str} to the current {\Coq} loadpath and
maps it to the logical directory {\dirpath}, which means that every
file {\tt M.v} physically lying in directory {\str} becomes accessible
through logical name ``{\dirpath}{\tt{.M}}''. 

\Rem {\tt Add LoadPath} also adds {\str} to the current ML loadpath.

\begin{Variants}
\item {\tt Add LoadPath {\str}.}\\
Performs as {\tt Add LoadPath {\str} as {\dirpath}} but for the empty directory path.
\end{Variants}

\subsection{\tt Add Rec LoadPath {\str} as {\dirpath}.}\comindex{Add Rec LoadPath}\label{AddRecLoadPath}
This command adds the directory {\str} and all its subdirectories 
to the current \Coq\ loadpath. The top directory {\str} is mapped to the logical directory {\dirpath} while any subdirectory {\textsl{pdir}} is mapped to logical directory {\dirpath}{\tt{.pdir}} and so on.

\Rem {\tt Add Rec LoadPath} also recursively adds {\str} to the current ML loadpath.

\begin{Variants}
\item {\tt Add Rec LoadPath {\str}.}\\
Works as {\tt Add Rec LoadPath {\str} as {\dirpath}} but for the empty logical directory path.
\end{Variants}

\subsection{\tt Remove LoadPath {\str}.}\comindex{Remove LoadPath}
This command removes the path {\str} from the current \Coq\ loadpath.

\subsection{\tt Print LoadPath.}\comindex{Print LoadPath}
This command displays the current \Coq\ loadpath.

\subsection{\tt Add ML Path {\str}.}\comindex{Add ML Path}
This command adds the path {\str} to the current Objective Caml loadpath (see
the command {\tt Declare ML Module} in the section \ref{compiled}).

\Rem This command is implied by {\tt Add LoadPath {\str} as {\dirpath}}.

\subsection{\tt Add Rec ML Path {\str}.}\comindex{Add Rec ML Path}
This command adds the directory {\str} and all its subdirectories 
to the current Objective Caml loadpath (see
the command {\tt Declare ML Module} in the section \ref{compiled}).

\Rem This command is implied by {\tt Add Rec LoadPath {\str} as {\dirpath}}.

\subsection{\tt Print ML Path {\str}.}\comindex{Print ML Path}
This command displays the current Objective Caml loadpath.
This command makes sense only under the bytecode version of {\tt
coqtop}, i.e. using option {\tt -byte} (see the
command {\tt Declare ML Module} in the section
\ref{compiled}).

\subsection{\tt Locate File {\str}.}\comindex{Locate
  File}\label{Locate File}
This command displays the location of file {\str} in the current loadpath.
Typically, {\str} is a \texttt{.cmo} or \texttt{.vo} or \texttt{.v} file.

\subsection{\tt Locate Library {\dirpath}.}
\comindex{Locate Library}
This command gives the status of the \Coq\ module {\dirpath}. It tells if the
module is loaded and if not searches in the load path for a module
of logical name {\dirpath}.

\section{States and Reset}

\subsection{\tt Reset \ident.}
\comindex{Reset}
This command removes all the objects in the environment since \ident\ 
was introduced, including \ident. \ident\ may be the name of a defined
or declared object as well as the name of a section.  One cannot reset
over the name of a module or of an object inside a module.

\begin{ErrMsgs}
\item \ident: \errindex{no such entry}
\end{ErrMsgs}

\subsection{\tt Back.}
\comindex{Back}

This commands undoes all the effects of the last vernacular
command. This does not include commands that only access to the
environment like those described in the previous sections of this
chapter (for instance {\tt Require} and {\tt Load} can be undone, but
not {\tt Check} and {\tt Locate}). Commands read from a vernacular
file are considered as a single command.

\begin{Variants}
\item {\tt Back $n$} \\
  Undoes $n$ vernacular commands.
\end{Variants}

\begin{ErrMsgs}
\item \errindex{Reached begin of command history} \\
  Happens when there is vernacular command to undo.
\end{ErrMsgs}

\subsection{\tt Restore State \ident.}
\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}).
\end{Variants}

\subsection{\tt Write State \str.}
\comindex{Write State}
Writes the current state into a file \str{} for
use in a further session. This file can be given as the {\tt
  inputstate} argument of the commands {\tt coqtop} and {\tt coqc}.

\begin{Variants}
\item {\tt Write State \ident}\\
 Equivalent to {\tt Write State "}{\ident}{\tt .coq".}.
 The state is saved in the current directory (see \pageref{Pwd}).
\end{Variants}

\section{Syntax facilities}

We present quickly in this section some syntactic facilities.
We will only sketch them here and refer the
interested reader to chapter \ref{Addoc-syntax} for more details and
examples.

\subsection{\tt Set Implicit Arguments.}
\comindex{Set Implicit Arguments}
\comindex{Unset Implicit Arguments}

This command sets the implicit argument mode on. Under this mode, the
arguments of declared constructions (constants, inductive types,
variables, ...) which can automatically be deduced from the others
arguments (typically type arguments in polymorphic functions) are
skipped. They are not printed and the user must not give them.  To
show what are the implicit arguments associated to a declaration
{\qualid}, use \texttt{Print \qualid}. You can change the implicit
arguments of a specific declaration by using the command
\texttt{Implicits} (see section \ref{Implicits}).  You can explicitely
give an argument which otherwise should be implicit by using the
symbol \verb=!= (see section \ref{Implicits-explicitation}).

To set the implicit argument mode off, use {\tt Unset Implicit Arguments.}

\begin{Variants}
\item {\tt Implicit Arguments On.}\comindex{Implicit Arguments On}\\
This is a deprecated equivalent to {\tt Set Implicit Arguments.} 
\item {\tt Implicit Arguments Off.}\comindex{Implicit Arguments Off}\\
This is a deprecated equivalent to {\tt Unset Implicit Arguments.} 
\end{Variants}

\SeeAlso section \ref{Auto-implicit}

\subsection{\tt Implicits {\qualid} [} \num$_1$ \ldots \num$_n$ {\tt ]}
\comindex{Implicits}
\label{Implicits}

This sets the implicit arguments of reference {\qualid} to be the
arguments at positions {\num$_1$ \ldots \num$_n$}. As a particular
case, if the list of numbers is empty then no implicit argument is
associated to {\qualid}.

\subsection{\tt Syntactic Definition {\ident} := \term.}
\comindex{Syntactic Definition}
\ttindex{?}
This command defines {\ident} as an
abbreviation with implicit arguments. Implicit arguments are denoted
in {\term} by {\tt ?} and they will have to be synthesized by the
system.

\Rem Since it may contain don't care variables {\tt ?}, the argument
{\term} cannot be typechecked at
definition time. But each of its subsequent usages will be.

\SeeAlso section \ref{Syntactic-Definition}


\subsection{\tt Syntax {\ident} {\rm\sl syntax-rules}.}
\comindex{Syntax}\index{Pretty printing}
This command addresses the extensible
pretty-printing mechanism of \Coq. It allows {\ident$_2$} to be 
pretty-printed as specified in {\rm\sl syntax-rules}. Many examples
of the {\tt Syntax} command usage may be found in the {\tt
  PreludeSyntax} file (see directory {\tt \$COQLIB/theories/INIT}).

\SeeAlso chapter \ref{Addoc-syntax}

\subsection{\tt Grammar \ident$_1$ \ident$_2$ := {\rm\sl
    grammar-rule}.}
\comindex{Grammar}\index{Extensive grammars}
This command allows to give explicitly new grammar rules for parsing
the user's own notation.  It may be used instead of the {\tt Syntactic
Definition} pragma.  It can also be used by an advanced \Coq's user
who programs his own tactics.

\SeeAlso chapters \ref{Addoc-syntax}

\subsection{\tt{Infix} {\num} {\str} {\qualid}.}\comindex{Infix}

This command declares the prefix operator denoted by {\qualid} as infix, with the
syntax {\term} {\str} {\term}. {\num} is the precedence associated to
the operator; it must lie between 1 and 10.  The infix operator \str\
associates to the left. {\str} must be a legal token. Both grammar
and pretty-print rules are automatically generated for {\str}.

\begin{Variants}
\item \texttt{Infix {\rm\sl assoc} {\num} {\str} {\qualid}.} \\
  Declares the full names denoted by {\qualid} as an infix operator with an alternate
  associativity. {\rm\sl assoc} may be one of {\tt LEFTA}, {\tt
  RIGHTA} and {\tt NONA}. The default is {\tt LEFTA}. When an
  associativity is given, the precedence level must lie between 6 and
  9. 
\end{Variants}

% Distfix not documented.

\section{Miscellaneous}

\subsection{\tt Quit.}\comindex{Quit}
This command permits to quit \Coq.

\subsection{\tt Drop.}\comindex{Drop}\label{Drop}

This is used mostly as a debug facility by \Coq's implementors
and does not concern the casual user.
This command permits to leave {\Coq} temporarily and enter the
Objective Caml toplevel. The Objective Caml command:

\begin{flushleft}
\begin{verbatim}
#use "include";;
\end{verbatim}
\end{flushleft}

\noindent add the right loadpaths and loads some toplevel printers for
all abstract types of \Coq - section\_path, identfifiers, terms, judgements,
\dots. You can also use the file \texttt{base\_include} instead,
that loads only the pretty-printers for section\_paths and
identifiers.
% See section \ref{test-and-debug} more information on the
% usage of the toplevel.
You can return back to \Coq{} with the command: 

\begin{flushleft}
\begin{verbatim}
go();;
\end{verbatim}
\end{flushleft}

\begin{Warnings}
\item It only works with the bytecode version of {\Coq} (i.e. {\tt coqtop} called with option {\tt -byte}, see page \pageref{binary-images}).
\item You must have compiled {\Coq} from the source package and set the
  environment variable \texttt{COQTOP} to the root of your copy of the sources (see section \ref{EnvVariables}).
\end{Warnings}

\subsection{\tt Set Silent.}
\comindex{Begin Silent}
\label{Begin-Silent}
\index{Silent mode}
This command turns off the normal displaying.

\subsection{\tt Unset Silent.}\comindex{End Silent}
This command turns the normal display on.

\subsection{\tt Time \textrm{\textsl{command}}.}\comindex{Time}
\label{time}
This command executes the vernac command \textrm{\textsl{command}}
and display the time needed to execute it.

%\subsection{\tt Explain ...}
%Not yet documented.

%\subsection{\tt Go ...}
%Not yet documented.

%\subsection{\tt Abstraction ...}
%Not yet documented.

% $Id$ 

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End: