1
\chapter{Vernacular commands}
2
\label{Vernacular-commands}
7
\subsection{\tt Print {\qualid}.}\comindex{Print}
8
This command displays on the screen informations about the declared or
9
defined object referred by {\qualid}.
12
\item {\qualid} \errindex{not a defined object}
16
\item {\tt Print Term {\qualid}.}
17
\comindex{Print Term}\\
18
This is a synonym to {\tt Print {\qualid}} when {\qualid} denotes a
21
\item {\tt About {\qualid}.}
24
This displays various informations about the object denoted by {\qualid}:
25
its kind (module, constant, assumption, inductive,
26
constructor, abbreviation\ldots), long name, type, implicit
27
arguments and argument scopes.
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.}\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}.}
59
This command displays the type of {\term}. When called in proof mode,
60
the term is checked in the local context of the current subgoal.
62
\subsection{\tt Eval {\rm\sl convtactic} in {\term}.}
65
This command performs the specified reduction on {\term}, and displays
66
the resulting term with its type. The term to be reduced may depend on
67
hypothesis introduced in the first subgoal (if a proof is in
70
\SeeAlso section~\ref{Conversion-tactics}.
72
\subsection{\tt Extraction \term.}
73
\label{ExtractionTerm}
75
This command displays the extracted term from
76
{\term}. The extraction is processed according to the distinction
77
between {\Set} and {\Prop}; that is to say, between logical and
78
computational content (see section \ref{Sorts}). The extracted term is
79
displayed in Objective Caml syntax, where global identifiers are still
80
displayed as in \Coq\ terms.
83
\item \texttt{Recursive Extraction {\qualid$_1$} \ldots{} {\qualid$_n$}.}\\
84
Recursively extracts all the material needed for the extraction of
85
globals {\qualid$_1$} \ldots{} {\qualid$_n$}.
88
\SeeAlso chapter~\ref{Extraction}.
90
\subsection{\tt Opaque \qualid$_1$ \dots \qualid$_n$.}
91
\comindex{Opaque}\label{Opaque} This command tells not to unfold the
92
the constants {\qualid$_1$} \dots {\qualid$_n$} in tactics using
93
$\delta$-conversion. Unfolding a constant is replacing it by its
94
definition. {\tt Opaque} can only apply on constants originally
95
defined as {\tt Transparent}.
97
Constants defined by a proof ended by {\tt Qed} are automatically
98
stamped as {\tt Opaque} and can no longer be considered as {\tt
99
Transparent}. This is to keep with the usual mathematical practice of
100
{\em proof irrelevance}: what matters in a mathematical development is
101
the sequence of lemma statements, not their actual proofs. This
102
distinguishes lemmas from the usual defined constants, whose actual
103
values are of course relevant in general.
105
\SeeAlso sections \ref{Conversion-tactics}, \ref{Automatizing},
109
\item \errindex{The reference \qualid\ was not found in the current
111
There is no constant referred by {\qualid} in the environment.
112
Nevertheless, if you asked \texttt{Opaque foo bar}
113
and if \texttt{bar} does not exist, \texttt{foo} is set opaque.
116
\subsection{\tt Transparent \qualid$_1$ \dots \qualid$_n$.}
117
\comindex{Transparent}\label{Transparent}
118
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.
120
The constants automatically declared transparent are the ones defined by a proof ended by {\tt Defined}, or by a {\tt
121
Definition} or {\tt Local} with an explicit body.
123
\Warning {\tt Transparent} and \texttt{Opaque} are not synchronous
124
with the reset mechanism. If a constant was transparent at point A, if
125
you set it opaque at point B and reset to point A, you return to state
126
of point A with the difference that the constant is still opaque. This
127
can cause changes in tactic scripts behaviour.
129
At section or module closing, a constant recovers the status it got at
130
the time of its definition.
132
%TODO: expliquer le rapport avec les sections
135
% \item \errindex{Can not set transparent.}\\
136
% It is a constant from a required module or a parameter.
137
\item \errindex{The reference \qualid\ was not found in the current
139
There is no constant referred by {\qualid} in the environment.
142
\SeeAlso sections \ref{Conversion-tactics}, \ref{Automatizing},
145
\subsection{\tt Search {\qualid}.}\comindex{Search}
146
This command displays the name and type of all theorems of the current
147
context whose statement's conclusion has the form {\tt ({\qualid} t1 ..
148
tn)}. This command is useful to remind the user of the name of
151
\item \errindex{The reference \qualid\ was not found in the current
153
There is no constant in the environment named \qualid.
158
{\tt Search {\qualid} inside {\module$_1$} \ldots{} {\module$_n$}.}
160
This restricts the search to constructions defined in modules
161
{\module$_1$} \ldots{} {\module$_n$}.
163
\item {\tt Search {\qualid} outside {\module$_1$} \ldots{} {\module$_n$}.}
165
This restricts the search to constructions not defined in modules
166
{\module$_1$} \ldots{} {\module$_n$}.
169
\item \errindex{Module/section \module{} not found}
170
No module \module{} has been required (see section~\ref{Require}).
175
\subsection{\tt SearchAbout {\qualid}.}\comindex{SearchAbout}
176
This command displays the name and type of all objects (theorems,
177
axioms, etc) of the current context whose statement contains \qualid.
178
This command is useful to remind the user of the name of library
182
\item \errindex{The reference \qualid\ was not found in the current
184
There is no constant in the environment named \qualid.
188
\item {\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{}
190
\noindent where {\textrm{\textsl{qualid-or-string}}} is a {\qualid} or
193
This extension of {\tt SearchAbout} searches for all objects whose
194
statement mentions all of {\qualid} of the list and whose name
195
contains all {\str} of the list.
200
Require Import ZArith.
201
SearchAbout [ Zmult Zplus "distr" ].
205
\begin{tabular}[t]{@{}l}
206
{\tt SearchAbout {\term} inside {\module$_1$} \ldots{} {\module$_n$}.} \\
207
{\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{} ]
208
inside {\module$_1$} \ldots{} {\module$_n$}.}
211
This restricts the search to constructions defined in modules
212
{\module$_1$} \ldots{} {\module$_n$}.
215
\begin{tabular}[t]{@{}l}
216
{\tt SearchAbout {\term} outside {\module$_1$}...{\module$_n$}.} \\
217
{\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{} ]
218
outside {\module$_1$}...{\module$_n$}.}
221
This restricts the search to constructions not defined in modules
222
{\module$_1$} \ldots{} {\module$_n$}.
226
\subsection{\tt SearchPattern {\term}.}\comindex{SearchPattern}
228
This command displays the name and type of all theorems of the current
229
context whose statement's conclusion matches the expression {\term}
230
where holes in the latter are denoted by ``{\texttt \_}''.
233
Require Import Arith.
234
SearchPattern (_ + _ = _ + _).
237
Patterns need not be linear: you can express that the same expression
238
must occur in two places by using pattern variables `{\texttt
242
Require Import Arith.
243
SearchPattern (?X1 + _ = _ + ?X1).
247
\item {\tt SearchPattern {\term} inside
248
{\module$_1$} \ldots{} {\module$_n$}.}\comindex{SearchPattern \ldots{} inside
251
This restricts the search to constructions defined in modules
252
{\module$_1$} \ldots{} {\module$_n$}.
254
\item {\tt SearchPattern {\term} outside {\module$_1$} \ldots{} {\module$_n$}.}\comindex{SearchPattern \ldots{} outside \ldots{}}
256
This restricts the search to constructions not defined in modules
257
{\module$_1$} \ldots{} {\module$_n$}.
261
\subsection{\tt SearchRewrite {\term}.}\comindex{SearchRewrite}
263
This command displays the name and type of all theorems of the current
264
context whose statement's conclusion is an equality of which one side matches
265
the expression {\term =}. Holes in {\term} are denoted by ``{\texttt \_}''.
268
Require Import Arith.
269
SearchRewrite (_ + _ + _).
273
\item {\tt SearchRewrite {\term} inside
274
{\module$_1$} \ldots{} {\module$_n$}.}
276
This restricts the search to constructions defined in modules
277
{\module$_1$} \ldots{} {\module$_n$}.
279
\item {\tt SearchRewrite {\term} outside {\module$_1$} \ldots{} {\module$_n$}.}
281
This restricts the search to constructions not defined in modules
282
{\module$_1$} \ldots{} {\module$_n$}.
286
% \subsection{\tt SearchIsos {\term}.}\comindex{SearchIsos}
288
% \texttt{SearchIsos} searches terms by their type modulo isomorphism.
289
% This command displays the full name of all constants, variables,
290
% inductive types, and inductive constructors of the current
291
% context whose type is isomorphic to {\term} modulo the contextual part of the
292
% following axiomatization (the mutual inductive types with one constructor,
293
% without implicit arguments, and for which projections exist, are regarded as a
294
% sequence of $\sa{}$):
298
% \ \ \ \ \=11.\ \=\kill
299
% \>1.\>$A=B\mx{ if }A\stackrel{\bt{}\io{}}{\lra{}}B$\\
300
% \>2.\>$\sa{}x:A.B=\sa{}y:A.B[x\la{}y]\mx{ if }y\not\in{}FV(\sa{}x:A.B)$\\
301
% \>3.\>$\Pi{}x:A.B=\Pi{}y:A.B[x\la{}y]\mx{ if }y\not\in{}FV(\Pi{}x:A.B)$\\
302
% \>4.\>$\sa{}x:A.B=\sa{}x:B.A\mx{ if }x\not\in{}FV(A,B)$\\
303
% \>5.\>$\sa{}x:(\sa{}y:A.B).C=\sa{}x:A.\sa{}y:B[y\la{}x].C[x\la{}(x,y)]$\\
304
% \>6.\>$\Pi{}x:(\sa{}y:A.B).C=\Pi{}x:A.\Pi{}y:B[y\la{}x].C[x\la{}(x,y)]$\\
305
% \>7.\>$\Pi{}x:A.\sa{}y:B.C=\sa{}y:(\Pi{}x:A.B).(\Pi{}x:A.C[y\la{}(y\sm{}x)]$\\
306
% \>8.\>$\sa{}x:A.unit=A$\\
307
% \>9.\>$\sa{}x:unit.A=A[x\la{}tt]$\\
308
% \>10.\>$\Pi{}x:A.unit=unit$\\
309
% \>11.\>$\Pi{}x:unit.A=A[x\la{}tt]$
312
% For more informations about the exact working of this command, see
315
\subsection{\tt Locate {\qualid}.}\comindex{Locate}
317
This command displays the full name of the qualified identifier {\qualid}
318
and consequently the \Coq\ module in which it is defined.
321
(*************** The last line should produce **************************)
322
(*********** Error: I.Dont.Exist not a defined object ******************)
325
Set Printing Depth 50.
330
Locate Init.Datatypes.O.
331
Locate Coq.Init.Datatypes.O.
335
\SeeAlso Section \ref{LocateSymbol}
337
\subsection{The {\sc Whelp} searching tool
340
{\sc Whelp} is an experimental searching and browsing tool for the
341
whole {\Coq} library and the whole set of {\Coq} user contributions.
342
{\sc Whelp} requires a browser to work. {\sc Whelp} has been developed
343
at the University of Bologna as part of the HELM\footnote{Hypertextual
344
Electronic Library of Mathematics} and MoWGLI\footnote{Mathematics on
345
the Web, Get it by Logics and Interfaces} projects. It can be invoked
346
directly from the {\Coq} toplevel or from {\CoqIDE}, assuming a
347
graphical environment is also running. The browser to use can be
348
selected by setting the environment variable {\tt
349
COQREMOTEBROWSER}. If not explicitly set, it defaults to
350
\verb!netscape -remote "OpenURL(%s)"! or
351
\verb!C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s!, depending on the
352
underlying operating system (in the command, the string \verb!%s!
353
serves as metavariable for the url to open).
355
The {\sc Whelp} commands are:
357
\subsubsection{\tt Whelp Locate "{\sl reg\_expr}".
358
\comindex{Whelp Locate}}
360
This command opens a browser window and displays the result of seeking
361
for all names that match the regular expression {\sl reg\_expr} in the
362
{\Coq} library and user contributions. The regular expression can
363
contain the special operators are * and ? that respectively stand for
364
an arbitrary substring and for exactly one character.
366
\variant {\tt Whelp Locate {\ident}.}\\
367
This is equivalent to {\tt Whelp Locate "{\ident}"}.
369
\subsubsection{\tt Whelp Match {\pattern}.
370
\comindex{Whelp Match}}
372
This command opens a browser window and displays the result of seeking
373
for all statements that match the pattern {\pattern}. Holes in the
374
pattern are represented by the wildcard character ``\_''.
376
\subsubsection{\tt Whelp Instance {\pattern}.}
377
\comindex{Whelp Instance}
379
This command opens a browser window and displays the result of seeking
380
for all statements that are instances of the pattern {\pattern}. The
381
pattern is here assumed to be an universally quantified expression.
383
\subsubsection{\tt Whelp Elim {\qualid}.}
384
\comindex{Whelp Elim}
386
This command opens a browser window and displays the result of seeking
387
for all statements that have the ``form'' of an elimination scheme
388
over the type denoted by {\qualid}.
390
\subsubsection{\tt Whelp Hint {\term}.}
391
\comindex{Whelp Hint}
393
This command opens a browser window and displays the result of seeking
394
for all statements that can be instantiated so that to prove the
397
\variant {\tt Whelp Hint.}\\ This is equivalent to {\tt Whelp Hint
398
{\sl goal}} where {\sl goal} is the current goal to prove. Notice that
399
{\Coq} does not send the local environment of definitions to the {\sc
400
Whelp} tool so that it only works on requests strictly based on, only,
401
definitions of the standard library and user contributions.
403
\section{Loading files}
405
\Coq\ offers the possibility of loading different
406
parts of a whole development stored in separate files. Their contents
407
will be loaded as if they were entered from the keyboard. This means
408
that the loaded files are ASCII files containing sequences of commands
409
for \Coq's toplevel. This kind of file is called a {\em script} for
410
\Coq\index{Script file}. The standard (and default) extension of
411
\Coq's script files is {\tt .v}.
413
\subsection{\tt Load {\ident}.}
414
\comindex{Load}\label{Load}
415
This command loads the file named {\ident}{\tt .v}, searching
416
successively in each of the directories specified in the {\em
417
loadpath}. (see section \ref{loadpath})
420
\item {\tt Load {\str}.}\label{Load-str}\\
421
Loads the file denoted by the string {\str}, where {\str} is any
422
complete filename. Then the \verb.~. and {\tt ..}
423
abbreviations are allowed as well as shell variables. If no
424
extension is specified, \Coq\ will use the default extension {\tt
426
\item {\tt Load Verbose {\ident}.},
427
{\tt Load Verbose {\str}}\\
428
\comindex{Load Verbose}
429
Display, while loading, the answers of \Coq\ to each command
430
(including tactics) contained in the loaded file
431
\SeeAlso section \ref{Begin-Silent}
435
\item \errindex{Can't find file {\ident} on loadpath}
438
\section{Compiled files}\label{compiled}\index{Compiled files}
440
This feature allows to build files for a quick loading. When loaded,
441
the commands contained in a compiled file will not be {\em replayed}.
442
In particular, proofs will not be replayed. This avoids a useless
445
\Rem A module containing an opened section cannot be compiled.
447
% \subsection{\tt Compile Module {\ident}.}
449
% \comindex{Compile Module}
451
% This command loads the file
452
% {\ident}{\tt .v} and plays the script it contains. Declarations,
453
% definitions and proofs it contains are {\em "packaged"} in a compiled
454
% form: the {\em module} named {\ident}.
455
% A file {\ident}{\tt .vo} is then created.
456
% The file {\ident}{\tt .v} is searched according to the
458
% The {\ident}{\tt .vo} is then written in the directory where
459
% {\ident}{\tt .v} was found.
462
% \item \texttt{Compile Module {\ident} {\str}.}\\
463
% Uses the file {\str}{\tt .v} or {\str} if the previous one does not
464
% exist to build the module {\ident}. In this case, {\str} is any
465
% string giving a filename in the UNIX sense (see section
467
% \Warning The given filename can not contain other caracters than
468
% the caracters of \Coq's identifiers : letters or digits or the
469
% underscore symbol ``\_''.
471
% \item \texttt{Compile Module Specification {\ident}.}\\
472
% \comindex{Compile Module Specification}
473
% Builds a specification module: only the types of terms are stored
474
% in the module. The bodies (the proofs) are {\em not} written
475
% in the module. In that case, the file created is {\ident}{\tt .vi}.
476
% This is only useful when proof terms take too much place in memory
477
% and are not necessary.
479
% \item \texttt{Compile Verbose Module {\ident}.}\\
480
% \comindex{Compile Verbose Module}
481
% Verbose version of Compile: shows the contents of the file being
485
% These different variants can be combined.
489
% \item \texttt{You cannot open a module when there are things other than}\\
490
% \texttt{Modules and Imports in the context.}\\
491
% The only commands allowed before a {Compile Module} command are {\tt
493
% {\tt Read Module} and {\tt Import}. Actually, The normal way to
494
% compile modules is by the {\tt coqc} command (see chapter
498
% \SeeAlso sections \ref{Opaque}, \ref{loadpath}, chapter
501
%\subsection{\tt Import {\qualid}.}\comindex{Import}
505
% Import and Export described in RefMan-mod.tex
506
% the minor difference (to avoid multiple Exporting of libraries) in
507
% the treatment of normal modules and libraries by Export omitted
510
\subsection{\tt Require {\dirpath}.}
514
This command looks in the loadpath for a file containing module
515
{\dirpath}, then loads and opens (imports) its contents.
516
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'}.
518
TODO: effect on the name table.
520
% The implementation file ({\ident}{\tt .vo}) is searched first,
521
% then the specification file ({\ident}{\tt .vi}) in case of failure.
522
If the module required has already been loaded, \Coq\
523
simply opens it (as {\tt Import {\dirpath}} would do it).
524
%If the module required is already loaded and open, \Coq\
525
%displays the following warning: {\tt {\ident} already imported}.
527
If a module {\it A} contains a command {\tt Require} {\it B} then the
528
command {\tt Require} {\it A} loads the module {\it B} but does not
529
open it (See the {\tt Require Export} variant below).
532
\item {\tt Require Export {\qualid}.}\\
533
\comindex{Require Export}
534
This command acts as {\tt Require} {\qualid}. But if a module {\it
535
A} contains a command {\tt Require Export} {\it B}, then the
536
command {\tt Require} {\it A} opens the module {\it B} as if the
537
user would have typed {\tt Require}{\it B}.
538
% \item {\tt Require $[$ Implementation $|$ Specification $]$ {\qualid}.}\\
539
% \comindex{Require Implementation}
540
% \comindex{Require Specification}
541
% Is the same as {\tt Require}, but specifying explicitly the
542
% implementation ({\tt.vo} file) or the specification ({\tt.vi}
546
% \item {\tt Require {\qualid} {\str}.}\\
547
% Specifies the file to load as being {\str} but containing module
549
% The opened module is still {\ident} and therefore must have been loaded.
550
\item {\tt Require {\qualid} {\str}.}\\
551
Specifies the file to load as being {\str} but containing module
552
{\qualid} which is then opened.
555
These different variants can be combined.
559
\item \errindex{Cannot load {\ident}: no physical path bound to {\dirpath}}
561
\item \errindex{Can't find module toto on loadpath}
563
The command did not find the file {\tt toto.vo}. Either {\tt
564
toto.v} exists but is not compiled or {\tt toto.vo} is in a directory
565
which is not in your {\tt LoadPath} (see section \ref{loadpath}).
567
\item \errindex{Bad magic number}
569
\index{Bad-magic-number@{\tt Bad Magic Number}}
570
The file {\tt{\ident}.vo} was found but either it is not a \Coq\
571
compiled module, or it was compiled with an older and incompatible
575
\SeeAlso chapter \ref{Addoc-coqc}
577
\subsection{\tt Print Modules.}
578
\comindex{Print Modules}
579
This command shows the currently loaded and currently opened
582
\subsection{\tt Declare ML Module {\str$_1$} .. {\str$_n$}.}
583
\comindex{Declare ML Module}
584
This commands loads the Objective Caml compiled files {\str$_1$} \dots
585
{\str$_n$} (dynamic link). It is mainly used to load tactics
587
% (see chapter \ref{WritingTactics}).
589
searched into the current Objective Caml loadpath (see the command {\tt
590
Add ML Path} in the section \ref{loadpath}). Loading of Objective Caml
591
files is only possible under the bytecode version of {\tt coqtop}
592
(i.e. {\tt coqtop} called with options {\tt -byte}, see chapter
596
\item \errindex{File not found on loadpath : \str}
597
\item \errindex{Loading of ML object file forbidden in a native Coq}
600
\subsection{\tt Print ML Modules.}\comindex{Print ML Modules}
601
This print the name of all \ocaml{} modules loaded with \texttt{Declare
602
ML Module}. To know from where these module were loaded, the user
603
should use the command \texttt{Locate File} (see page \pageref{Locate File})
606
\label{loadpath}\index{Loadpath}
608
There are currently two loadpaths in \Coq. A loadpath where seeking
609
{\Coq} files (extensions {\tt .v} or {\tt .vo} or {\tt .vi}) and one where
610
seeking Objective Caml files. The default loadpath contains the
611
directory ``\texttt{.}'' denoting the current directory and mapped to the empty logical path (see section \ref{LongNames}).
613
\subsection{\tt Pwd.}\comindex{Pwd}\label{Pwd}
614
This command displays the current working directory.
616
\subsection{\tt Cd {\str}.}\comindex{Cd}
617
This command changes the current directory according to {\str}
618
which can be any valid path.
622
Is equivalent to {\tt Pwd.}
625
\subsection{\tt Add LoadPath {\str} as {\dirpath}.}
626
\comindex{Add LoadPath}\label{AddLoadPath}
628
This command adds the path {\str} to the current {\Coq} loadpath and
629
maps it to the logical directory {\dirpath}, which means that every
630
file {\tt M.v} physically lying in directory {\str} becomes accessible
631
through logical name ``{\dirpath}{\tt{.M}}''.
633
\Rem {\tt Add LoadPath} also adds {\str} to the current ML loadpath.
636
\item {\tt Add LoadPath {\str}.}\\
637
Performs as {\tt Add LoadPath {\str} as {\dirpath}} but for the empty directory path.
640
\subsection{\tt Add Rec LoadPath {\str} as {\dirpath}.}\comindex{Add Rec LoadPath}\label{AddRecLoadPath}
641
This command adds the directory {\str} and all its subdirectories
642
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.
644
\Rem {\tt Add Rec LoadPath} also recursively adds {\str} to the current ML loadpath.
647
\item {\tt Add Rec LoadPath {\str}.}\\
648
Works as {\tt Add Rec LoadPath {\str} as {\dirpath}} but for the empty logical directory path.
651
\subsection{\tt Remove LoadPath {\str}.}\comindex{Remove LoadPath}
652
This command removes the path {\str} from the current \Coq\ loadpath.
654
\subsection{\tt Print LoadPath.}\comindex{Print LoadPath}
655
This command displays the current \Coq\ loadpath.
657
\subsection{\tt Add ML Path {\str}.}\comindex{Add ML Path}
658
This command adds the path {\str} to the current Objective Caml loadpath (see
659
the command {\tt Declare ML Module} in the section \ref{compiled}).
661
\Rem This command is implied by {\tt Add LoadPath {\str} as {\dirpath}}.
663
\subsection{\tt Add Rec ML Path {\str}.}\comindex{Add Rec ML Path}
664
This command adds the directory {\str} and all its subdirectories
665
to the current Objective Caml loadpath (see
666
the command {\tt Declare ML Module} in the section \ref{compiled}).
668
\Rem This command is implied by {\tt Add Rec LoadPath {\str} as {\dirpath}}.
670
\subsection{\tt Print ML Path {\str}.}\comindex{Print ML Path}
671
This command displays the current Objective Caml loadpath.
672
This command makes sense only under the bytecode version of {\tt
673
coqtop}, i.e. using option {\tt -byte} (see the
674
command {\tt Declare ML Module} in the section
677
\subsection{\tt Locate File {\str}.}\comindex{Locate
678
File}\label{Locate File}
679
This command displays the location of file {\str} in the current loadpath.
680
Typically, {\str} is a \texttt{.cmo} or \texttt{.vo} or \texttt{.v} file.
682
\subsection{\tt Locate Library {\dirpath}.}
683
\comindex{Locate Library}
684
This command gives the status of the \Coq\ module {\dirpath}. It tells if the
685
module is loaded and if not searches in the load path for a module
686
of logical name {\dirpath}.
688
\section{States and Reset}
690
\subsection{\tt Reset \ident.}
692
This command removes all the objects in the environment since \ident\
693
was introduced, including \ident. \ident\ may be the name of a defined
694
or declared object as well as the name of a section. One cannot reset
695
over the name of a module or of an object inside a module.
698
\item \ident: \errindex{no such entry}
701
\subsection{\tt Back.}
704
This commands undoes all the effects of the last vernacular
705
command. This does not include commands that only access to the
706
environment like those described in the previous sections of this
707
chapter (for instance {\tt Require} and {\tt Load} can be undone, but
708
not {\tt Check} and {\tt Locate}). Commands read from a vernacular
709
file are considered as a single command.
712
\item {\tt Back $n$} \\
713
Undoes $n$ vernacular commands.
717
\item \errindex{Reached begin of command history} \\
718
Happens when there is vernacular command to undo.
721
\subsection{\tt Restore State \str.}
722
\comindex{Restore State}
723
Restores the state contained in the file \str.
726
\item {\tt Restore State \ident}\\
727
Equivalent to {\tt Restore State "}{\ident}{\tt .coq"}.
728
\item {\tt Reset Initial.}\comindex{Reset Initial}\\
729
Goes back to the initial state (like after the command {\tt coqtop},
730
when the interactive session began). This command is only available
734
\subsection{\tt Write State \str.}
735
\comindex{Write State}
736
Writes the current state into a file \str{} for
737
use in a further session. This file can be given as the {\tt
738
inputstate} argument of the commands {\tt coqtop} and {\tt coqc}.
741
\item {\tt Write State \ident}\\
742
Equivalent to {\tt Write State "}{\ident}{\tt .coq"}.
743
The state is saved in the current directory (see \pageref{Pwd}).
746
\section{Quitting and debugging}
748
\subsection{\tt Quit.}\comindex{Quit}
749
This command permits to quit \Coq.
751
\subsection{\tt Drop.}\comindex{Drop}\label{Drop}
753
This is used mostly as a debug facility by \Coq's implementors
754
and does not concern the casual user.
755
This command permits to leave {\Coq} temporarily and enter the
756
Objective Caml toplevel. The Objective Caml command:
764
\noindent add the right loadpaths and loads some toplevel printers for
765
all abstract types of \Coq - section\_path, identfifiers, terms, judgements,
766
\dots. You can also use the file \texttt{base\_include} instead,
767
that loads only the pretty-printers for section\_paths and
769
% See section \ref{test-and-debug} more information on the
770
% usage of the toplevel.
771
You can return back to \Coq{} with the command:
780
\item It only works with the bytecode version of {\Coq} (i.e. {\tt coqtop} called with option {\tt -byte}, see page \pageref{binary-images}).
781
\item You must have compiled {\Coq} from the source package and set the
782
environment variable \texttt{COQTOP} to the root of your copy of the sources (see section \ref{EnvVariables}).
785
\subsection{\tt Time \textrm{\textsl{command}}.}\comindex{Time}
787
This command executes the vernac command \textrm{\textsl{command}}
788
and display the time needed to execute it.
790
\section{Controlling display}
792
\subsection{\tt Set Silent.}
793
\comindex{Begin Silent}
796
This command turns off the normal displaying.
798
\subsection{\tt Unset Silent.}\comindex{End Silent}
799
This command turns the normal display on.
801
\subsection{\tt Set Printing Width {\integer}.}\comindex{Set Printing Width}
802
This command sets which left-aligned part of the width of the screen
805
\subsection{\tt Unset Printing Width.}\comindex{Unset Printing Width}
806
This command resets the width of the screen used for display to its
807
default value (which is 78 at the time of writing this documentation).
809
\subsection{\tt Test Printing Width.}\comindex{Test Printing Width}
810
This command displays the current screen width used for display.
812
\subsection{\tt Set Printing Depth {\integer}.}\comindex{Set Printing Depth}
813
This command sets the nesting depth of the formatter used for
814
pretty-printing. Beyond this depth, display of subterms is replaced by
817
\subsection{\tt Unset Printing Depth.}\comindex{Unset Printing Depth}
818
This command resets the nesting depth of the formatter used for
819
pretty-printing to its default value (at the
820
time of writing this documentation, the default value is 50).
822
\subsection{\tt Test Printing Depth.}\comindex{Test Printing Depth}
823
This command displays the current nesting depth used for display.
825
%\subsection{\tt Explain ...}
828
%\subsection{\tt Go ...}
831
%\subsection{\tt Abstraction ...}
834
\section{Controlling the conversion algorithm}
836
{\Coq} comes with two algorithms to check the convertibility of types
837
(see section~\ref{convertibility}). The first algorithm lazily
838
compares applicative terms while the other is a brute-force but efficient
839
algorithm that first normalizes the terms before comparing them. The
840
second algorithm is based on a bytecode representation of terms
841
similar to the bytecode representation used in the ZINC virtual
842
machine~\cite{Leroy90}. It is specially useful for intensive
843
computation of algebraic values, such as numbers, and for reflexion-based
846
\subsection{\tt Set Virtual Machine
847
\label{SetVirtualMachine}
848
\comindex{Set Virtual Machine}}
850
This activates the bytecode-based conversion algorithm.
852
\subsection{\tt Unset Virtual Machine
853
\comindex{Unset Virtual Machine}}
855
This deactivates the bytecode-based conversion algorithm.
857
\subsection{\tt Test Virtual Machine
858
\comindex{Test Virtual Machine}}
860
This tells if the bytecode-based conversion algorithm is
861
activated. The default behavior is to have the bytecode-based
862
conversion algorithm deactivated.
864
\SeeAlso sections~\ref{vmcompute} and~\ref{vmoption}.
866
% $Id: RefMan-oth.tex 9044 2006-07-12 13:22:17Z herbelin $
870
%%% TeX-master: "Reference-Manual"
added
removed
refman/RefMan-oth.tex
