1
\chapter[Vernacular commands]{Vernacular commands\label{Vernacular-commands}
2
\label{Other-commands}}
6
\subsection[\tt Print {\qualid}.]{\tt Print {\qualid}.\comindex{Print}}
7
This command displays on the screen informations about the declared or
8
defined object referred by {\qualid}.
11
\item {\qualid} \errindex{not a defined object}
15
\item {\tt Print Term {\qualid}.}
16
\comindex{Print Term}\\
17
This is a synonym to {\tt Print {\qualid}} when {\qualid} denotes a
20
\item {\tt About {\qualid}.}
23
This displays various informations about the object denoted by {\qualid}:
24
its kind (module, constant, assumption, inductive,
25
constructor, abbreviation\ldots), long name, type, implicit
26
arguments and argument scopes. It does not print the body of
27
definitions or proofs.
29
%\item {\tt Print Proof {\qualid}.}\comindex{Print Proof}\\
30
%In case \qualid\ denotes an opaque theorem defined in a section,
31
%it is stored on a special unprintable form and displayed as
32
%{\tt <recipe>}. {\tt Print Proof} forces the printable form of \qualid\
33
%to be computed and displays it.
36
\subsection[\tt Print All.]{\tt Print All.\comindex{Print All}}
37
This command displays informations about the current state of the
38
environment, including sections and modules.
41
\item {\tt Inspect \num.}\comindex{Inspect}\\
42
This command displays the {\num} last objects of the current
43
environment, including sections and modules.
44
\item {\tt Print Section {\ident}.}\comindex{Print Section}\\
45
should correspond to a currently open section, this command
46
displays the objects defined since the beginning of this section.
48
%% \item {\tt Print.}\comindex{Print}\\
49
%% This command displays the axioms and variables declarations in the
50
%% environment as well as the constants defined since the last variable
54
\section{Requests to the environment}
56
\subsection[\tt Check {\term}.]{\tt Check {\term}.\label{Check}
58
This command displays the type of {\term}. When called in proof mode,
59
the term is checked in the local context of the current subgoal.
61
\subsection[\tt Eval {\rm\sl convtactic} in {\term}.]{\tt Eval {\rm\sl convtactic} in {\term}.\comindex{Eval}}
63
This command performs the specified reduction on {\term}, and displays
64
the resulting term with its type. The term to be reduced may depend on
65
hypothesis introduced in the first subgoal (if a proof is in
68
\SeeAlso Section~\ref{Conversion-tactics}.
70
\subsection[\tt Extraction \term.]{\tt Extraction \term.\label{ExtractionTerm}
71
\comindex{Extraction}}
72
This command displays the extracted term from
73
{\term}. The extraction is processed according to the distinction
74
between {\Set} and {\Prop}; that is to say, between logical and
75
computational content (see Section~\ref{Sorts}). The extracted term is
76
displayed in Objective Caml syntax, where global identifiers are still
77
displayed as in \Coq\ terms.
80
\item \texttt{Recursive Extraction {\qualid$_1$} \ldots{} {\qualid$_n$}.}\\
81
Recursively extracts all the material needed for the extraction of
82
globals {\qualid$_1$} \ldots{} {\qualid$_n$}.
85
\SeeAlso Chapter~\ref{Extraction}.
87
\subsection[\tt Print Assumptions {\qualid}.]{\tt Print Assumptions {\qualid}.\comindex{Print Assumptions}}
88
\label{PrintAssumptions}
90
This commands display all the assumptions (axioms, parameters and
91
variables) a theorem or definition depends on. Especially, it informs
92
on the assumptions with respect to which the validity of a theorem
95
\subsection[\tt Search {\qualid}.]{\tt Search {\qualid}.\comindex{Search}}
96
This command displays the name and type of all theorems of the current
97
context whose statement's conclusion has the form {\tt ({\qualid} t1 ..
98
tn)}. This command is useful to remind the user of the name of
101
\item \errindex{The reference \qualid\ was not found in the current
103
There is no constant in the environment named \qualid.
108
{\tt Search {\qualid} inside {\module$_1$} \ldots{} {\module$_n$}.}
110
This restricts the search to constructions defined in modules
111
{\module$_1$} \ldots{} {\module$_n$}.
113
\item {\tt Search {\qualid} outside {\module$_1$} \ldots{} {\module$_n$}.}
115
This restricts the search to constructions not defined in modules
116
{\module$_1$} \ldots{} {\module$_n$}.
119
\item \errindex{Module/section \module{} not found}
120
No module \module{} has been required (see Section~\ref{Require}).
125
\subsection[\tt SearchAbout {\qualid}.]{\tt SearchAbout {\qualid}.\comindex{SearchAbout}}
126
This command displays the name and type of all objects (theorems,
127
axioms, etc) of the current context whose statement contains \qualid.
128
This command is useful to remind the user of the name of library
132
\item \errindex{The reference \qualid\ was not found in the current
134
There is no constant in the environment named \qualid.
137
\newcommand{\termpatternorstr}{{\termpattern}\textrm{\textsl{-}}{\str}}
140
\item {\tt SearchAbout {\str}.}
142
If {\str} is a valid identifier, this command displays the name and type
143
of all objects (theorems, axioms, etc) of the current context whose
144
name contains {\str}. If {\str} is a notation's string denoting some
145
reference {\qualid} (referred to by its main symbol as in \verb="+"=
146
or by its notation's string as in \verb="_ + _"= or \verb="_ 'U' _"=, see
147
Section~\ref{Notation}), the command works like {\tt SearchAbout
150
\item {\tt SearchAbout {\str}\%{\delimkey}.}
152
The string {\str} must be a notation or the main symbol of a notation
153
which is then interpreted in the scope bound to the delimiting key
154
{\delimkey} (see Section~\ref{scopechange}).
156
\item {\tt SearchAbout {\termpattern}.}
158
This searches for all statements or types of definition that contains
159
a subterm that matches the pattern {\termpattern} (holes of the
160
pattern are either denoted by ``{\texttt \_}'' or
161
by ``{\texttt ?{\ident}}'' when non linear patterns are expected).
163
\item {\tt SearchAbout [ \nelist{\zeroone{-}{\termpatternorstr}}{}
166
\noindent where {\termpatternorstr} is a
167
{\termpattern} or a {\str}, or a {\str} followed by a scope
168
delimiting key {\tt \%{\delimkey}}.
170
This generalization of {\tt SearchAbout} searches for all objects
171
whose statement or type contains a subterm matching {\termpattern} (or
172
{\qualid} if {\str} is the notation for a reference {\qualid}) and
173
whose name contains all {\str} of the request that correspond to valid
174
identifiers. If a {\termpattern} or a {\str} is prefixed by ``-'', the
175
search excludes the objects that mention that {\termpattern} or that
179
\begin{tabular}[t]{@{}l}
180
{\tt SearchAbout {\termpatternorstr} inside {\module$_1$} \ldots{} {\module$_n$}.} \\
181
{\tt SearchAbout [ \nelist{{\termpatternorstr}}{} ]
182
inside {\module$_1$} \ldots{} {\module$_n$}.}
185
This restricts the search to constructions defined in modules
186
{\module$_1$} \ldots{} {\module$_n$}.
189
\begin{tabular}[t]{@{}l}
190
{\tt SearchAbout {\termpatternorstr} outside {\module$_1$}...{\module$_n$}.} \\
191
{\tt SearchAbout [ \nelist{{\termpatternorstr}}{} ]
192
outside {\module$_1$}...{\module$_n$}.}
195
This restricts the search to constructions not defined in modules
196
{\module$_1$} \ldots{} {\module$_n$}.
203
Require Import ZArith.
206
SearchAbout [ Zmult Zplus "distr" ].
207
SearchAbout [ "+"%Z "*"%Z "distr" -positive -Prop].
208
SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas.
211
\subsection[\tt SearchPattern {\termpattern}.]{\tt SearchPattern {\term}.\comindex{SearchPattern}}
213
This command displays the name and type of all theorems of the current
214
context whose statement's conclusion matches the expression {\term}
215
where holes in the latter are denoted by ``{\texttt \_}''. It is a
216
variant of {\tt SearchAbout {\termpattern}} that does not look for
217
subterms but searches for statements whose conclusion has exactly the
221
Require Import Arith.
222
SearchPattern (_ + _ = _ + _).
225
Patterns need not be linear: you can express that the same expression
226
must occur in two places by using pattern variables `{\texttt
230
Require Import Arith.
231
SearchPattern (?X1 + _ = _ + ?X1).
235
\item {\tt SearchPattern {\term} inside
236
{\module$_1$} \ldots{} {\module$_n$}.}
238
This restricts the search to constructions defined in modules
239
{\module$_1$} \ldots{} {\module$_n$}.
241
\item {\tt SearchPattern {\term} outside {\module$_1$} \ldots{} {\module$_n$}.}
243
This restricts the search to constructions not defined in modules
244
{\module$_1$} \ldots{} {\module$_n$}.
248
\subsection[\tt SearchRewrite {\term}.]{\tt SearchRewrite {\term}.\comindex{SearchRewrite}}
250
This command displays the name and type of all theorems of the current
251
context whose statement's conclusion is an equality of which one side matches
252
the expression {\term}. Holes in {\term} are denoted by ``{\texttt \_}''.
255
Require Import Arith.
256
SearchRewrite (_ + _ + _).
260
\item {\tt SearchRewrite {\term} inside
261
{\module$_1$} \ldots{} {\module$_n$}.}
263
This restricts the search to constructions defined in modules
264
{\module$_1$} \ldots{} {\module$_n$}.
266
\item {\tt SearchRewrite {\term} outside {\module$_1$} \ldots{} {\module$_n$}.}
268
This restricts the search to constructions not defined in modules
269
{\module$_1$} \ldots{} {\module$_n$}.
273
% \subsection[\tt SearchIsos {\term}.]{\tt SearchIsos {\term}.\comindex{SearchIsos}}
275
% \texttt{SearchIsos} searches terms by their type modulo isomorphism.
276
% This command displays the full name of all constants, variables,
277
% inductive types, and inductive constructors of the current
278
% context whose type is isomorphic to {\term} modulo the contextual part of the
279
% following axiomatization (the mutual inductive types with one constructor,
280
% without implicit arguments, and for which projections exist, are regarded as a
281
% sequence of $\sa{}$):
285
% \ \ \ \ \=11.\ \=\kill
286
% \>1.\>$A=B\mx{ if }A\stackrel{\bt{}\io{}}{\lra{}}B$\\
287
% \>2.\>$\sa{}x:A.B=\sa{}y:A.B[x\la{}y]\mx{ if }y\not\in{}FV(\sa{}x:A.B)$\\
288
% \>3.\>$\Pi{}x:A.B=\Pi{}y:A.B[x\la{}y]\mx{ if }y\not\in{}FV(\Pi{}x:A.B)$\\
289
% \>4.\>$\sa{}x:A.B=\sa{}x:B.A\mx{ if }x\not\in{}FV(A,B)$\\
290
% \>5.\>$\sa{}x:(\sa{}y:A.B).C=\sa{}x:A.\sa{}y:B[y\la{}x].C[x\la{}(x,y)]$\\
291
% \>6.\>$\Pi{}x:(\sa{}y:A.B).C=\Pi{}x:A.\Pi{}y:B[y\la{}x].C[x\la{}(x,y)]$\\
292
% \>7.\>$\Pi{}x:A.\sa{}y:B.C=\sa{}y:(\Pi{}x:A.B).(\Pi{}x:A.C[y\la{}(y\sm{}x)]$\\
293
% \>8.\>$\sa{}x:A.unit=A$\\
294
% \>9.\>$\sa{}x:unit.A=A[x\la{}tt]$\\
295
% \>10.\>$\Pi{}x:A.unit=unit$\\
296
% \>11.\>$\Pi{}x:unit.A=A[x\la{}tt]$
299
% For more informations about the exact working of this command, see
302
\subsection[\tt Locate {\qualid}.]{\tt Locate {\qualid}.\comindex{Locate}
304
This command displays the full name of the qualified identifier {\qualid}
305
and consequently the \Coq\ module in which it is defined.
308
(*************** The last line should produce **************************)
309
(*********** Error: I.Dont.Exist not a defined object ******************)
312
Set Printing Depth 50.
317
Locate Init.Datatypes.O.
318
Locate Coq.Init.Datatypes.O.
322
\SeeAlso Section \ref{LocateSymbol}
324
\subsection{The {\sc Whelp} searching tool
327
{\sc Whelp} is an experimental searching and browsing tool for the
328
whole {\Coq} library and the whole set of {\Coq} user contributions.
329
{\sc Whelp} requires a browser to work. {\sc Whelp} has been developed
330
at the University of Bologna as part of the HELM\footnote{Hypertextual
331
Electronic Library of Mathematics} and MoWGLI\footnote{Mathematics on
332
the Web, Get it by Logics and Interfaces} projects. It can be invoked
333
directly from the {\Coq} toplevel or from {\CoqIDE}, assuming a
334
graphical environment is also running. The browser to use can be
335
selected by setting the environment variable {\tt
336
COQREMOTEBROWSER}. If not explicitly set, it defaults to
337
\verb!firefox -remote \"OpenURL(%s,new-tab)\" || firefox %s &"! or
338
\verb!C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s!, depending on the
339
underlying operating system (in the command, the string \verb!%s!
340
serves as metavariable for the url to open).
341
The Whelp tool relies on a dedicated Whelp server and on another server
342
called Getter that retrieves formal documents. The default Whelp server name
343
can be obtained using the command {\tt Test Whelp Server}
344
\comindex{Test Whelp Server} and the default Getter can be obtained
345
using the command: {\tt Test Whelp Getter} \comindex{Test Whelp
346
Getter}. The Whelp server name can be changed using the command:
349
\noindent {\tt Set Whelp Server {\str}}.\\
350
where {\str} is a URL (e.g. {\tt http://mowgli.cs.unibo.it:58080}).
351
\comindex{Set Whelp Server}
354
\noindent The Getter can be changed using the command:
357
\noindent {\tt Set Whelp Getter {\str}}.\\
358
where {\str} is a URL (e.g. {\tt http://mowgli.cs.unibo.it:58081}).
359
\comindex{Set Whelp Getter}
363
The {\sc Whelp} commands are:
365
\subsubsection{\tt Whelp Locate "{\sl reg\_expr}".
366
\comindex{Whelp Locate}}
368
This command opens a browser window and displays the result of seeking
369
for all names that match the regular expression {\sl reg\_expr} in the
370
{\Coq} library and user contributions. The regular expression can
371
contain the special operators are * and ? that respectively stand for
372
an arbitrary substring and for exactly one character.
374
\variant {\tt Whelp Locate {\ident}.}\\
375
This is equivalent to {\tt Whelp Locate "{\ident}"}.
377
\subsubsection{\tt Whelp Match {\pattern}.
378
\comindex{Whelp Match}}
380
This command opens a browser window and displays the result of seeking
381
for all statements that match the pattern {\pattern}. Holes in the
382
pattern are represented by the wildcard character ``\_''.
384
\subsubsection[\tt Whelp Instance {\pattern}.]{\tt Whelp Instance {\pattern}.\comindex{Whelp Instance}}
386
This command opens a browser window and displays the result of seeking
387
for all statements that are instances of the pattern {\pattern}. The
388
pattern is here assumed to be an universally quantified expression.
390
\subsubsection[\tt Whelp Elim {\qualid}.]{\tt Whelp Elim {\qualid}.\comindex{Whelp Elim}}
392
This command opens a browser window and displays the result of seeking
393
for all statements that have the ``form'' of an elimination scheme
394
over the type denoted by {\qualid}.
396
\subsubsection[\tt Whelp Hint {\term}.]{\tt Whelp Hint {\term}.\comindex{Whelp Hint}}
398
This command opens a browser window and displays the result of seeking
399
for all statements that can be instantiated so that to prove the
402
\variant {\tt Whelp Hint.}\\ This is equivalent to {\tt Whelp Hint
403
{\sl goal}} where {\sl goal} is the current goal to prove. Notice that
404
{\Coq} does not send the local environment of definitions to the {\sc
405
Whelp} tool so that it only works on requests strictly based on, only,
406
definitions of the standard library and user contributions.
408
\section{Loading files}
410
\Coq\ offers the possibility of loading different
411
parts of a whole development stored in separate files. Their contents
412
will be loaded as if they were entered from the keyboard. This means
413
that the loaded files are ASCII files containing sequences of commands
414
for \Coq's toplevel. This kind of file is called a {\em script} for
415
\Coq\index{Script file}. The standard (and default) extension of
416
\Coq's script files is {\tt .v}.
418
\subsection[\tt Load {\ident}.]{\tt Load {\ident}.\comindex{Load}\label{Load}}
419
This command loads the file named {\ident}{\tt .v}, searching
420
successively in each of the directories specified in the {\em
421
loadpath}. (see Section~\ref{loadpath})
424
\item {\tt Load {\str}.}\label{Load-str}\\
425
Loads the file denoted by the string {\str}, where {\str} is any
426
complete filename. Then the \verb.~. and {\tt ..}
427
abbreviations are allowed as well as shell variables. If no
428
extension is specified, \Coq\ will use the default extension {\tt
430
\item {\tt Load Verbose {\ident}.},
431
{\tt Load Verbose {\str}}\\
432
\comindex{Load Verbose}
433
Display, while loading, the answers of \Coq\ to each command
434
(including tactics) contained in the loaded file
435
\SeeAlso Section~\ref{Begin-Silent}
439
\item \errindex{Can't find file {\ident} on loadpath}
442
\section[Compiled files]{Compiled files\label{compiled}\index{Compiled files}}
444
This section describes the commands used to load compiled files (see
445
Chapter~\ref{Addoc-coqc} for documentation on how to compile a file).
446
A compiled file is a particular case of module called {\em library file}.
449
% Import and Export described in RefMan-mod.tex
450
% the minor difference (to avoid multiple Exporting of libraries) in
451
% the treatment of normal modules and libraries by Export omitted
453
\subsection[\tt Require {\qualid}.]{\tt Require {\qualid}.\label{Require}
456
This command looks in the loadpath for a file containing
457
module {\qualid} and adds the corresponding module to the environment
458
of {\Coq}. As library files have dependencies in other library files,
459
the command {\tt Require {\qualid}} recursively requires all library
460
files the module {\qualid} depends on and adds the corresponding modules to the
461
environment of {\Coq} too. {\Coq} assumes that the compiled files have
462
been produced by a valid {\Coq} compiler and their contents are then not
463
replayed nor rechecked.
465
To locate the file in the file system, {\qualid} is decomposed under
466
the form {\dirpath}{\tt .}{\textsl{ident}} and the file {\ident}{\tt
467
.vo} is searched in the physical directory of the file system that is
468
mapped in {\Coq} loadpath to the logical path {\dirpath} (see
469
Section~\ref{loadpath}). The mapping between physical directories and
470
logical names at the time of requiring the file must be consistent
471
with the mapping used to compile the file.
474
\item {\tt Require Import {\qualid}.} \comindex{Require}
476
This loads and declares the module {\qualid} and its dependencies
477
then imports the contents of {\qualid} as described in
478
Section~\ref{Import}.
480
It does not import the modules on which {\qualid} depends unless
481
these modules were itself required in module {\qualid} using {\tt
482
Require Export}, as described below, or recursively required through
483
a sequence of {\tt Require Export}.
485
If the module required has already been loaded, {\tt Require Import
486
{\qualid}} simply imports it, as {\tt Import {\qualid}} would.
488
\item {\tt Require Export {\qualid}.}
489
\comindex{Require Export}
491
This command acts as {\tt Require Import} {\qualid}, but if a
492
further module, say {\it A}, contains a command {\tt Require
493
Export} {\it B}, then the command {\tt Require Import} {\it A}
494
also imports the module {\it B}.
496
\item {\tt Require \zeroone{Import {\sl |} Export} {\qualid}$_1$ \ldots {\qualid}$_n$.}
498
This loads the modules {\qualid}$_1$, \ldots, {\qualid}$_n$ and
499
their recursive dependencies. If {\tt Import} or {\tt Export} is
500
given, it also imports {\qualid}$_1$, \ldots, {\qualid}$_n$ and all
501
the recursive dependencies that were marked or transitively marked
504
\item {\tt Require \zeroone{Import {\sl |} Export} {\str}.}
506
This shortcuts the resolution of the qualified name into a library
507
file name by directly requiring the module to be found in file
513
\item \errindex{Cannot load {\qualid}: no physical path bound to {\dirpath}}
515
\item \errindex{Cannot find library foo in loadpath}
517
The command did not find the file {\tt foo.vo}. Either {\tt
518
foo.v} exists but is not compiled or {\tt foo.vo} is in a directory
519
which is not in your {\tt LoadPath} (see Section~\ref{loadpath}).
521
\item \errindex{Compiled library {\ident}.vo makes inconsistent assumptions over library {\qualid}}
523
The command tried to load library file {\ident}.vo that depends on
524
some specific version of library {\qualid} which is not the one
525
already loaded in the current {\Coq} session. Probably {\ident}.v
526
was not properly recompiled with the last version of the file
527
containing module {\qualid}.
529
\item \errindex{Bad magic number}
531
\index{Bad-magic-number@{\tt Bad Magic Number}}
532
The file {\tt{\ident}.vo} was found but either it is not a \Coq\
533
compiled module, or it was compiled with an older and incompatible
536
\item \errindex{The file {\ident}.vo contains library {\dirpath} and not
539
The library file {\dirpath'} is indirectly required by the {\tt
540
Require} command but it is bound in the current loadpath to the file
541
{\ident}.vo which was bound to a different library name {\dirpath}
542
at the time it was compiled.
546
\SeeAlso Chapter~\ref{Addoc-coqc}
548
\subsection[\tt Print Libraries.]{\tt Print Libraries.\comindex{Print Libraries}}
550
This command displays the list of library files loaded in the current
551
{\Coq} session. For each of these libraries, it also tells if it is
554
\subsection[\tt Declare ML Module {\str$_1$} .. {\str$_n$}.]{\tt Declare ML Module {\str$_1$} .. {\str$_n$}.\comindex{Declare ML Module}}
555
This commands loads the Objective Caml compiled files {\str$_1$} \dots
556
{\str$_n$} (dynamic link). It is mainly used to load tactics
558
% (see Chapter~\ref{WritingTactics}).
560
searched into the current Objective Caml loadpath (see the command {\tt
561
Add ML Path} in the Section~\ref{loadpath}). Loading of Objective Caml
562
files is only possible under the bytecode version of {\tt coqtop}
563
(i.e. {\tt coqtop} called with options {\tt -byte}, see chapter
564
\ref{Addoc-coqc}), or when Coq has been compiled with a version of
565
Objective Caml that supports native {\tt Dynlink} ($\ge$ 3.11).
568
\item \errindex{File not found on loadpath : \str}
569
\item \errindex{Loading of ML object file forbidden in a native Coq}
572
\subsection[\tt Print ML Modules.]{\tt Print ML Modules.\comindex{Print ML Modules}}
573
This print the name of all \ocaml{} modules loaded with \texttt{Declare
574
ML Module}. To know from where these module were loaded, the user
575
should use the command \texttt{Locate File} (see Section~\ref{Locate File})
577
\section[Loadpath]{Loadpath\label{loadpath}\index{Loadpath}}
579
There are currently two loadpaths in \Coq. A loadpath where seeking
580
{\Coq} files (extensions {\tt .v} or {\tt .vo} or {\tt .vi}) and one where
581
seeking Objective Caml files. The default loadpath contains the
582
directory ``\texttt{.}'' denoting the current directory and mapped to the empty logical path (see Section~\ref{LongNames}).
584
\subsection[\tt Pwd.]{\tt Pwd.\comindex{Pwd}\label{Pwd}}
585
This command displays the current working directory.
587
\subsection[\tt Cd {\str}.]{\tt Cd {\str}.\comindex{Cd}}
588
This command changes the current directory according to {\str}
589
which can be any valid path.
593
Is equivalent to {\tt Pwd.}
596
\subsection[\tt Add LoadPath {\str} as {\dirpath}.]{\tt Add LoadPath {\str} as {\dirpath}.\comindex{Add LoadPath}\label{AddLoadPath}}
598
This command adds the physical directory {\str} to the current {\Coq}
599
loadpath and maps it to the logical directory {\dirpath}, which means
600
that every file \textrm{\textsl{dirname}}/\textrm{\textsl{basename.v}}
601
physically lying in subdirectory {\str}/\textrm{\textsl{dirname}}
602
becomes accessible in {\Coq} through absolute logical name
603
{\dirpath}{\tt .}\textrm{\textsl{dirname}}{\tt
604
.}\textrm{\textsl{basename}}.
606
\Rem {\tt Add LoadPath} also adds {\str} to the current ML loadpath.
609
\item {\tt Add LoadPath {\str}.}\\
610
Performs as {\tt Add LoadPath {\str} as {\dirpath}} but for the empty directory path.
613
\subsection[\tt Add Rec LoadPath {\str} as {\dirpath}.]{\tt Add Rec LoadPath {\str} as {\dirpath}.\comindex{Add Rec LoadPath}\label{AddRecLoadPath}}
614
This command adds the physical directory {\str} and all its subdirectories to
615
the current \Coq\ loadpath. The top directory {\str} is mapped to the
616
logical directory {\dirpath} and any subdirectory {\textsl{pdir}} of it is
617
mapped to logical name {\dirpath}{\tt .}\textsl{pdir} and
618
recursively. Subdirectories corresponding to invalid {\Coq}
619
identifiers are skipped, and, by convention, subdirectories named {\tt
620
CVS} or {\tt \_darcs} are skipped too.
622
Otherwise, said, {\tt Add Rec LoadPath {\str} as {\dirpath}} behaves
623
as {\tt Add LoadPath {\str} as {\dirpath}} excepts that files lying in
624
validly named subdirectories of {\str} need not be qualified to be
627
In case of files with identical base name, files lying in most recently
628
declared {\dirpath} are found first and explicit qualification is
629
required to refer to the other files of same base name.
631
If several files with identical base name are present in different
632
subdirectories of a recursive loadpath declared via a single instance of
633
{\tt Add Rec LoadPath}, which of these files is found first is
634
system-dependent and explicit qualification is recommended.
636
\Rem {\tt Add Rec LoadPath} also recursively adds {\str} to the current ML loadpath.
639
\item {\tt Add Rec LoadPath {\str}.}\\
640
Works as {\tt Add Rec LoadPath {\str} as {\dirpath}} but for the empty logical directory path.
643
\subsection[\tt Remove LoadPath {\str}.]{\tt Remove LoadPath {\str}.\comindex{Remove LoadPath}}
644
This command removes the path {\str} from the current \Coq\ loadpath.
646
\subsection[\tt Print LoadPath.]{\tt Print LoadPath.\comindex{Print LoadPath}}
647
This command displays the current \Coq\ loadpath.
650
\item {\tt Print LoadPath {\dirpath}.}\\
651
Works as {\tt Print LoadPath} but displays only the paths that extend the {\dirpath} prefix.
654
\subsection[\tt Add ML Path {\str}.]{\tt Add ML Path {\str}.\comindex{Add ML Path}}
655
This command adds the path {\str} to the current Objective Caml loadpath (see
656
the command {\tt Declare ML Module} in the Section~\ref{compiled}).
658
\Rem This command is implied by {\tt Add LoadPath {\str} as {\dirpath}}.
660
\subsection[\tt Add Rec ML Path {\str}.]{\tt Add Rec ML Path {\str}.\comindex{Add Rec ML Path}}
661
This command adds the directory {\str} and all its subdirectories
662
to the current Objective Caml loadpath (see
663
the command {\tt Declare ML Module} in the Section~\ref{compiled}).
665
\Rem This command is implied by {\tt Add Rec LoadPath {\str} as {\dirpath}}.
667
\subsection[\tt Print ML Path {\str}.]{\tt Print ML Path {\str}.\comindex{Print ML Path}}
668
This command displays the current Objective Caml loadpath.
669
This command makes sense only under the bytecode version of {\tt
670
coqtop}, i.e. using option {\tt -byte} (see the
671
command {\tt Declare ML Module} in the section
674
\subsection[\tt Locate File {\str}.]{\tt Locate File {\str}.\comindex{Locate
675
File}\label{Locate File}}
676
This command displays the location of file {\str} in the current loadpath.
677
Typically, {\str} is a \texttt{.cmo} or \texttt{.vo} or \texttt{.v} file.
679
\subsection[\tt Locate Library {\dirpath}.]{\tt Locate Library {\dirpath}.\comindex{Locate Library}\label{Locate Library}}
680
This command gives the status of the \Coq\ module {\dirpath}. It tells if the
681
module is loaded and if not searches in the load path for a module
682
of logical name {\dirpath}.
684
\section{States and Reset}
686
\subsection[\tt Reset \ident.]{\tt Reset \ident.\comindex{Reset}}
687
This command removes all the objects in the environment since \ident\
688
was introduced, including \ident. \ident\ may be the name of a defined
689
or declared object as well as the name of a section. One cannot reset
690
over the name of a module or of an object inside a module.
693
\item \ident: \errindex{no such entry}
696
\subsection[\tt Back.]{\tt Back.\comindex{Back}}
698
This commands undoes all the effects of the last vernacular
699
command. This does not include commands that only access to the
700
environment like those described in the previous sections of this
701
chapter (for instance {\tt Require} and {\tt Load} can be undone, but
702
not {\tt Check} and {\tt Locate}). Commands read from a vernacular
703
file are considered as a single command.
706
\item {\tt Back $n$} \\
707
Undoes $n$ vernacular commands.
711
\item \errindex{Reached begin of command history} \\
712
Happens when there is vernacular command to undo.
715
\subsection[\tt Backtrack $\num_1$ $\num_2$ $\num_3$.]{\tt Backtrack $\num_1$ $\num_2$ $\num_3$.\comindex{Backtrack}}
717
This command is dedicated for the use in graphical interfaces. It
718
allows to backtrack to a particular \emph{global} state, i.e.
719
typically a state corresponding to a previous line in a script. A
720
global state includes declaration environment but also proof
721
environment (see Chapter~\ref{Proof-handling}). The three numbers
722
$\num_1$, $\num_2$ and $\num_3$ represent the following:
724
\item $\num_3$: Number of \texttt{Abort} to perform, i.e. the number
725
of currently opened nested proofs that must be canceled (see
726
Chapter~\ref{Proof-handling}).
727
\item $\num_2$: \emph{Proof state number} to unbury once aborts have
728
been done. Coq will compute the number of \texttt{Undo} to perform
729
(see Chapter~\ref{Proof-handling}).
730
\item $\num_1$: Environment state number to unbury, Coq will compute
731
the number of \texttt{Back} to perform.
735
\subsubsection{How to get state numbers?}
736
\label{sec:statenums}
739
Notice that when in \texttt{-emacs} mode, \Coq\ displays the current
740
proof and environment state numbers in the prompt. More precisely the
741
prompt in \texttt{-emacs} mode is the following:
743
\verb!<prompt>! \emph{$id_i$} \verb!<! $\num_1$
744
\verb!|! $id_1$\verb!|!$id_2$\verb!|!\dots\verb!|!$id_n$
745
\verb!|! $\num_2$ \verb!< </prompt>!
750
\item \emph{$id_i$} is the name of the current proof (if there is
751
one, otherwise \texttt{Coq} is displayed, see
752
Chapter~\ref{Proof-handling}).
753
\item $\num_1$ is the environment state number after the last
755
\item $\num_2$ is the proof state number after the last
757
\item $id_1$ $id_2$ \dots $id_n$ are the currently opened proof names
758
(order not significant).
761
It is then possible to compute the \texttt{Backtrack} command to
762
unbury the state corresponding to a particular prompt. For example,
763
suppose the current prompt is:
765
\verb!<! goal4 \verb!<! 35
766
\verb!|!goal1\verb!|!goal4\verb!|!goal3\verb!|!goal2\verb!|!
767
\verb!|!8 \verb!< </prompt>!
769
and we want to backtrack to a state labeled by:
771
\verb!<! goal2 \verb!<! 32
772
\verb!|!goal1\verb!|!goal2
773
\verb!|!12 \verb!< </prompt>!
775
We have to perform \verb!Backtrack 32 12 2! , i.e. perform 2
776
\texttt{Abort}s (to cancel goal4 and goal3), then rewind proof until
777
state 12 and finally go back to environment state 32. Notice that this
778
supposes that proofs are nested in a regular way (no \texttt{Resume} or
779
\texttt{Suspend} commands).
782
\item {\tt BackTo n}. \comindex{BackTo}\\
783
Is a more basic form of \texttt{Backtrack} where only the first
784
argument (global environment number) is given, no \texttt{abort} and
785
no \texttt{Undo} is performed.
788
\subsection[\tt Restore State \str.]{\tt Restore State \str.\comindex{Restore State}}
789
Restores the state contained in the file \str.
792
\item {\tt Restore State \ident}\\
793
Equivalent to {\tt Restore State "}{\ident}{\tt .coq"}.
794
\item {\tt Reset Initial.}\comindex{Reset Initial}\\
795
Goes back to the initial state (like after the command {\tt coqtop},
796
when the interactive session began). This command is only available
800
\subsection[\tt Write State \str.]{\tt Write State \str.\comindex{Write State}}
801
Writes the current state into a file \str{} for
802
use in a further session. This file can be given as the {\tt
803
inputstate} argument of the commands {\tt coqtop} and {\tt coqc}.
806
\item {\tt Write State \ident}\\
807
Equivalent to {\tt Write State "}{\ident}{\tt .coq"}.
808
The state is saved in the current directory (see Section~\ref{Pwd}).
811
\section{Quitting and debugging}
813
\subsection[\tt Quit.]{\tt Quit.\comindex{Quit}}
814
This command permits to quit \Coq.
816
\subsection[\tt Drop.]{\tt Drop.\comindex{Drop}\label{Drop}}
818
This is used mostly as a debug facility by \Coq's implementors
819
and does not concern the casual user.
820
This command permits to leave {\Coq} temporarily and enter the
821
Objective Caml toplevel. The Objective Caml command:
829
\noindent add the right loadpaths and loads some toplevel printers for
830
all abstract types of \Coq - section\_path, identifiers, terms, judgments,
831
\dots. You can also use the file \texttt{base\_include} instead,
832
that loads only the pretty-printers for section\_paths and
834
% See Section~\ref{test-and-debug} more information on the
835
% usage of the toplevel.
836
You can return back to \Coq{} with the command:
845
\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}).
846
\item You must have compiled {\Coq} from the source package and set the
847
environment variable \texttt{COQTOP} to the root of your copy of the sources (see Section~\ref{EnvVariables}).
850
\subsection[\tt Time \textrm{\textsl{command}}.]{\tt Time \textrm{\textsl{command}}.\comindex{Time}
852
This command executes the vernacular command \textrm{\textsl{command}}
853
and display the time needed to execute it.
855
\section{Controlling display}
857
\subsection[\tt Set Silent.]{\tt Set Silent.\comindex{Set Silent}
860
This command turns off the normal displaying.
862
\subsection[\tt Unset Silent.]{\tt Unset Silent.\comindex{Unset Silent}}
863
This command turns the normal display on.
865
\subsection[\tt Set Printing Width {\integer}.]{\tt Set Printing Width {\integer}.\comindex{Set Printing Width}}
866
This command sets which left-aligned part of the width of the screen
869
\subsection[\tt Unset Printing Width.]{\tt Unset Printing Width.\comindex{Unset Printing Width}}
870
This command resets the width of the screen used for display to its
871
default value (which is 78 at the time of writing this documentation).
873
\subsection[\tt Test Printing Width.]{\tt Test Printing Width.\comindex{Test Printing Width}}
874
This command displays the current screen width used for display.
876
\subsection[\tt Set Printing Depth {\integer}.]{\tt Set Printing Depth {\integer}.\comindex{Set Printing Depth}}
877
This command sets the nesting depth of the formatter used for
878
pretty-printing. Beyond this depth, display of subterms is replaced by
881
\subsection[\tt Unset Printing Depth.]{\tt Unset Printing Depth.\comindex{Unset Printing Depth}}
882
This command resets the nesting depth of the formatter used for
883
pretty-printing to its default value (at the
884
time of writing this documentation, the default value is 50).
886
\subsection[\tt Test Printing Depth.]{\tt Test Printing Depth.\comindex{Test Printing Depth}}
887
This command displays the current nesting depth used for display.
889
%\subsection{\tt Explain ...}
892
%\subsection{\tt Go ...}
895
%\subsection{\tt Abstraction ...}
898
\section{Controlling the reduction strategies and the conversion algorithm}
900
{\Coq} provides reduction strategies that the tactics can invoke and
901
two different algorithms to check the convertibility of types.
902
The first conversion algorithm lazily
903
compares applicative terms while the other is a brute-force but efficient
904
algorithm that first normalizes the terms before comparing them. The
905
second algorithm is based on a bytecode representation of terms
906
similar to the bytecode representation used in the ZINC virtual
907
machine~\cite{Leroy90}. It is specially useful for intensive
908
computation of algebraic values, such as numbers, and for reflexion-based
909
tactics. The commands to fine-tune the reduction strategies and the
910
lazy conversion algorithm are described first.
912
\subsection[\tt Opaque \qualid$_1$ \dots \qualid$_n$.]{\tt Opaque \qualid$_1$ \dots \qualid$_n$.\comindex{Opaque}\label{Opaque}}
913
This command has an effect on unfoldable constants, i.e.
914
on constants defined by {\tt Definition} or {\tt Let} (with an explicit
915
body), or by a command assimilated to a definition such as {\tt
916
Fixpoint}, {\tt Program Definition}, etc, or by a proof ended by {\tt
917
Defined}. The command tells not to unfold
918
the constants {\qualid$_1$} \dots {\qualid$_n$} in tactics using
919
$\delta$-conversion (unfolding a constant is replacing it by its
922
{\tt Opaque} has also on effect on the conversion algorithm of {\Coq},
923
telling to delay the unfolding of a constant as later as possible in
924
case {\Coq} has to check the conversion (see Section~\ref{conv-rules})
925
of two distinct applied constants.
927
The scope of {\tt Opaque} is limited to the current section, or
928
current file, unless the variant {\tt Global Opaque \qualid$_1$ \dots
929
\qualid$_n$} is used.
931
\SeeAlso sections \ref{Conversion-tactics}, \ref{Automatizing},
935
\item \errindex{The reference \qualid\ was not found in the current
937
There is no constant referred by {\qualid} in the environment.
938
Nevertheless, if you asked \texttt{Opaque foo bar}
939
and if \texttt{bar} does not exist, \texttt{foo} is set opaque.
942
\subsection[\tt Transparent \qualid$_1$ \dots \qualid$_n$.]{\tt Transparent \qualid$_1$ \dots \qualid$_n$.\comindex{Transparent}\label{Transparent}}
943
This command is the converse of {\tt Opaque} and it applies on
944
unfoldable constants to restore their unfoldability after an {\tt
947
Note in particular that constants defined by a proof ended by {\tt
948
Qed} are not unfoldable and {\tt Transparent} has no effect on
949
them. This is to keep with the usual mathematical practice of {\em
950
proof irrelevance}: what matters in a mathematical development is the
951
sequence of lemma statements, not their actual proofs. This
952
distinguishes lemmas from the usual defined constants, whose actual
953
values are of course relevant in general.
955
The scope of {\tt Transparent} is limited to the current section, or
956
current file, unless the variant {\tt Global Transparent \qualid$_1$
957
\dots \qualid$_n$} is used.
960
% \item \errindex{Can not set transparent.}\\
961
% It is a constant from a required module or a parameter.
962
\item \errindex{The reference \qualid\ was not found in the current
964
There is no constant referred by {\qualid} in the environment.
967
\SeeAlso sections \ref{Conversion-tactics}, \ref{Automatizing},
970
\subsection{\tt Strategy {\it level} [ \qualid$_1$ \dots \qualid$_n$
971
].\comindex{Strategy}\comindex{Local Strategy}\label{Strategy}}
972
This command generalizes the behavior of {\tt Opaque} and {\tt
973
Transparent} commands. It is used to fine-tune the strategy for
974
unfolding constants, both at the tactic level and at the kernel
975
level. This command associates a level to \qualid$_1$ \dots
976
\qualid$_n$. Whenever two expressions with two distinct head
977
constants are compared (for instance, this comparison can be triggered
978
by a type cast), the one with lower level is expanded first. In case
979
of a tie, the second one (appearing in the cast type) is expanded.
981
Levels can be one of the following (higher to lower):
983
\item[opaque]: level of opaque constants. They cannot be expanded by
984
tactics (behaves like $+\infty$, see next item).
985
\item[\num]: levels indexed by an integer. Level $0$ corresponds
986
to the default behavior, which corresponds to transparent
987
constants. This level can also be referred to as {\bf transparent}.
988
Negative levels correspond to constants to be expanded before normal
989
transparent constants, while positive levels correspond to constants
990
to be expanded after normal transparent constants.
991
\item[expand]: level of constants that should be expanded first
992
(behaves like $-\infty$)
995
These directives survive section and module closure, unless the
996
command is prefixed by {\tt Local}. In the latter case, the behavior
997
regarding sections and modules is the same as for the {\tt
998
Transparent} and {\tt Opaque} commands.
1000
\subsection{\tt Set Virtual Machine
1001
\label{SetVirtualMachine}
1002
\comindex{Set Virtual Machine}}
1004
This activates the bytecode-based conversion algorithm.
1006
\subsection{\tt Unset Virtual Machine
1007
\comindex{Unset Virtual Machine}}
1009
This deactivates the bytecode-based conversion algorithm.
1011
\subsection{\tt Test Virtual Machine
1012
\comindex{Test Virtual Machine}}
1014
This tells if the bytecode-based conversion algorithm is
1015
activated. The default behavior is to have the bytecode-based
1016
conversion algorithm deactivated.
1018
\SeeAlso sections~\ref{vmcompute} and~\ref{vmoption}.
1020
% $Id: RefMan-oth.tex 12112 2009-04-28 15:47:34Z herbelin $
1022
%%% Local Variables:
1024
%%% TeX-master: "Reference-Manual"
added
removed
doc/refman/RefMan-oth.tex
