Next: Isabelle Proof General, Previous: LEGO Proof General, Up: Top [Contents][Index]
Coq Proof General is an instantiation of Proof General for the Coq proof assistant. It supports most of the generic features of Proof General.
Coq Proof General supplies the following key-bindings:
Inserts “intros ” and also introduces the name of the hypothesis proposed by coq on the current goal.
Show the goal (enter for the current goal, i <enter> for the ith goal).
Add the prefix C-u to see the answer with all pretty printing options temporarily disable (Set Printing All).
Prompts for “Check ” query arguments, the default input name is built from the identifier under the cursor.
Add the prefix C-u to see the answer with all pretty printing options temporarily disable (Set Printing All).
The same for a “Print ” query.
The same for a “About ” query.
The same for a “SearchAbout ” query (no C-u prefix).
The same for a Search “SearchIsos” (no C-u prefix).
Inserts “End <section-name>.” (this should work well with nested sections).
The Coq project file is the recommended way to configure the Coq
load path and the mapping of logical module names to physical
file path’. The project file is typically named
_CoqProject
and must be located at the directory root of
your Coq project. Proof General searches for the Coq project file
starting at the current directory and walking the directory
structure upwards. The Coq project file contains the common
options (especially -R
) and a list of the files of the
project, see the Coq reference manual, Section 15.3, “Creating a
Makefile for Coq modules”.
The Coq project file should contain something like:
-R foo bar -I foo2 -arg -foo3 file.v bar/other_file.v ...
Proof General only extracts the common options from the Coq
project file and uses them for coqtop
background
processes as well as for coqdep
and coqc
when you use
the auto compilation feature, Automatic Compilation in Detail. For the example above, Proof General will start
coqtop -foo3 -R foo bar -I foo2
.
Remarque: -arg
must be followed by one and only one option
to pass to coqtop/coqc, use several -arg
to issue several
options. One per line (limitation of Proof General).
For backward compatibility, one can also configure the load path
with the option coq-load-path
, but this is not compatible
with CoqIde
or coq_makefile
.
To change the name of the Coq project file, configure
coq-project-filename
(select menu Proof-General ->
Advanced -> Customize -> Coq
and scroll down to “Coq Project
Filename”). Customizing coq-project-filename
this way
will change the Coq project file name permanently and globally.
If you only want to change the name of the Coq project file for
one project you can set the option as local file variable,
Using file variables. This can be done either directly in
every file or once for all files of a directory tree with a
.dir-local.el
file, See (emacs)Directory Variables.
The file .dir-local.el
should then contain
((coq-mode . ((coq-project-filename . "myprojectfile"))))
Note that variables set in .dir-local.el
are automatically
made buffer local (such that files in different directories can
have their independent setting of coq-project-filename
).
If you make complex customizations using eval
in
.dir-local.el
, you might want to add appropriate calls to
make-local-variable
.
Documentation of the user option coq-project-filename
:
The name of coq project file.
The coq project file of a coq developpement (Cf Coq documentation
on "makefile generation") should contain the arguments given to
coq_makefile. In particular it contains the -I and -R
options (preferably one per line). If ‘coq-use-coqproject’ is
t (default) the content of this file will be used by proofgeneral
to infer the ‘coq-load-path
’ and the ‘coq-prog-args
’ variables
that set the coqtop invocation by proofgeneral. This is now the
recommended way of configuring the coqtop invocation. Local file
variables may still be used to override the coq project file’s
configuration. .dir-locals.el files also work and override
project file settings.
To disable the Coq project file feature in Proof General, set
coq-use-project-file
to nil (select menu
Proof-General -> Advanced -> Customize -> Coq
and scroll
down to “Coq Use Project File”).
If t, when opening a coq file read the dominating _CoqProject.
If t, when a coq file is opened, Proof General will look for a
project file (see ‘coq-project-filename
’) somewhere in the
current directory or its parent directories. If there is one,
its contents are read and used to determine the arguments that
must be given to coqtop. In particular it sets the load
path (including the -R lib options) (see ‘coq-load-path
’).
You can also use the .dir-locals.el as above to configure this setting on a per project basis.
Since version 4.1 Coq Proof General has multiple file support. It consists of the following points:
coqtop
when changing the active scripting bufferDifferent buffers may require different load path’ or different
sets of -I
options. Because Coq cannot undo changes in the
load path, Proof General is forced to restart coqtop
when
the active scripting buffer changes.
Locking those buffers on which the current active scripting
buffer depends. This is controlled by the user option
coq-lock-ancestors
,
Customizing Coq Multiple File Support and
Locking Ancestors.
Before a Require
command is processed it may be necessary
to save and compile some buffers. Because this feature
conflicts with existing customization habits, it is switched off
by default. When it is properly configured, one can freely switch
between different buffers. Proof General will compile the
necessary files whenever a Require
command is processed.
The compilation feature does currently not support ML modules.
There are actually two implementations of the Recompilation feature.
With parallel compilation, coqdep and coqc are launched in the background and Proof General stays responsive during compilation. Up to ‘coq-max-background-compilation-jobs’ coqdep and coqc processes may run in parallel. Coq 8.5 quick compilation is supported with various modes, Quick compilation and .vio Files.
With synchronous compilation, coqdep and coqc are called synchronously for each Require command. Proof General is locked until the compilation finishes. Coq 8.5 quick compilation is not supported with synchronously compilation.
To enable the automatic compilation feature, you have to follow these points:
coq-compile-before-require
(menu Coq
-> Auto Compilation -> Compile Before Require
) to enable
compilation before processing Require
commands and set
coq-compile-parallel-in-background
(menu Coq
-> Auto Compilation -> Parallel background compilation
) for
parallel asynchronous compilation (recommended).
coq-load-path
. -I
or -R
options in
coq-prog-name
or coq-prog-args
must be deleted.
coq-max-background-compilation-jobs
if you want to limit
the number of parallel background jobs and set
coq-compile-keep-going
(menu Coq -> Auto Compilation
-> Keep going
) to let compilation continue after the first
error.
To abort parallel background compilation, use C-c C-c
(proof-interrupt-process
), the tool bar interrupt icon,
the menu entry Abort Background Compilation
(menu
Coq -> Auto Compilation
) or kill the Coq toplevel via
C-c C-x
(proof-shell-exit
). To abort synchronous
single threaded compilation, simply hit C-g
.
When coq-compile-before-require
is enabled, Proof
General looks for Require
commands in text that gets
asserted (i.e., in text that is moved from the editing region to
the queue region, Locked queue and editing regions). If
Proof General finds a Require
command, it checks the
dependencies and (re-)compiles files as necessary. The Require
command and the following text is only sent to Coq after the
compilation finished.
Declare ML Module
commands are currently not recognized.
Proof General uses coqdep
in order to translate the
qualified identifiers in Require
commands to coq library
file names and to determine library dependencies. Because Proof
General cannot know whether files are updated outside of Emacs,
it checks for every Require
command the complete
dependency tree and recompiles files as necessary.
Output from the compilation is only shown in case
of errors. It then appears in the buffer
*coq-compile-response*
.
One can use C-x `
(bound to next-error
,
See (emacs)Compilation Mode) to jump to error locations.
Sometimes the compilation commands do not produce error messages
with location information, then C-x `
does only work in a
limited way.
For Coq version 8.5 or newer, the option coq-compile-quick
controls how -quick
and .vio
files are used,
Quick compilation and .vio Files. This can also be
configured in the menu Coq -> Auto Compilation
.
Similar to make -k
, background compilation can be
configured to continue as far as possible after the first error,
see option coq-compile-keep-going
(menu Coq -> Auto
Compilation -> Keep going
). The keep-going option only applies
to errors from coqdep
and coqc
. For all other
errors (for instance when the translation from logical module
names to physical files fails or when starting coqc
or
coqdep
fails), the compilation is immediately aborted.
When a Require
command causes a compilation of some files,
one may wish to save some buffers to disk beforehand. The option
coq-compile-auto-save
controls how and which files are
saved. There are two orthogonal choices: One may wish to save all
or only the Coq source files, and, one may or may not want to
confirm the saving of each file.
With ‘coq-compile-parallel-in-background’ (menu Coq ->
Settings -> Compile Parallel In Background
) you can choose
between two implementations of internal compilation.
This is the old, now outdated version supported since Proof General
4.1. This method starts coqdep and coqc processes one after each
other in synchronous subprocesses. Your Emacs session will be
locked until compilation finishes. Use C-g
to interrupt
compilation. This method supports compilation via an external
command (such as make
), see option
coq-compile-command
in Customizing Coq Multiple File Support below. Synchronous compilation does not support the
quick compilation of Coq 8.5.
This is the newer and default version added in Proof General version 4.3. It
runs up to coq-max-background-compilation-jobs
coqdep and
coqc jobs in parallel in asynchronous subprocesses (or uses all
your CPU cores if coq-max-background-compilation-jobs
equals 'all-cpus
). Your Emacs will stay responsive during
compilation. To abort the background compilation process, use
C-c C-c
(proof-interrupt-process
), the tool bar
interrupt icon, the menu entry Abort Background
Compilation
(menu Coq -> Auto Compilation
) or kill the
Coq toplevel via C-c C-x
(proof-shell-exit
).
For the usual case, you have at most ‘coq-max-background-compilation-jobs’ parallel processes including your Proof General process. The usual case applies, when the Require commands are the first commands in the file. If you have other commands between two Require commands or before the first Require, then you may see Proof General and Coq running in addition to ‘coq-max-background-compilation-jobs’ compilation jobs.
Depending on the setting of coq-compile-quick
(which can
also be set via menu Coq -> Auto Compilation
) Proof
General produces .vio
or .vo
files and deletes
outdated .vio
or .vo
files to ensure Coq does not
load outdated files. When quick-and-vio2vo
is selected a
vio2vo compilation starts when the Require
command had
been processed, Quick compilation and .vio Files.
Actually, even with this method, not everything runs asynchronously. To translate module identifiers from the Coq sources into file names, Proof General runs coqdep on an automatically generated, one-line file. These coqdep jobs run synchronously while the Require commands are parsed. The coqdep jobs on the real source files do run asynchronously in the background.
Locking ancestor files works as a side effect of dependency checking. This means that ancestor locking does only work when Proof General performs dependency checking and compilation itself. If an external command is used, Proof General does not see all dependencies and can therefore only lock direct ancestors.
In the default setting,
when you want to edit a locked ancestor, you are
forced to completely retract the current scripting buffer.
You can simplify this by setting proof-strict-read-only
to
'retract
(menu Proof-General -> Quick Options ->
Read Only -> Undo On Edit
). Then typing in some ancestor will
immediately retract you current scripting buffer and unlock that
ancestor.
You have two choices, if you don’t like ancestor locking in its
default way.
You can either switch ancestor locking completely off via
coq-lock-ancestors
(Customizing Coq Multiple File Support) or you can generally permit editing in locked
sections with selecting
Proof-General
-> Quick Options
-> Read Only
-> Freely Edit
(which will set the option
proof-strict-read-only
to nil
).
[The right behaviour for Coq, namely to retract the current
scripting buffer only up to the appropriate Require
command, would be quite difficult to implement in the current
Proof General infrastructure. Further, it has only dubious
benefit, as Require commands are usually on the top of each
file.]
Proof General supports quick compilation only with the parallel
asynchronous compilation. There are 4 modes that can be
configured with coq-compile-quick
or by selecting one of
the radio buttons in the Coq -> Auto Compilation
menu.
Use the default no-quick
, if you have not yet switched to
Proof using
. Use quick-no-vio2vo
, if you want quick
recompilation without producing .vo files. Option
quick-and-vio2vo
recompiles with -quick
as
quick-no-vio2vo
does, but schedules a vio2vo compilation
for missing .vo
files after a certain delay. Finally, use
ensure-vo
for only importing .vo
files with
complete universe checks.
Note that with all of no-quick
, quick-no-vio2vo
and
quick-and-vio2vo
your development might be unsound because
universe constraints are not fully present in .vio
files.
There are a few peculiarities of quick compilation in Coq 8.5 that one should be aware of.
Proof using
.
.vio
files. You can speed up
quick compilation noticeably by running on a RAM disk.
.vo
and the .vio
files are present,
Coq load the more recent one, regardless of whether
-quick
, and emits a warning when the .vio
is more
recent than the .vo
.
.vio
file of some library was present are not compatible
with (other) files compiled when also the .vo
file of that
library was present, see Coq issue #5223 for details. As a rule
of thumb one should run vio2vo compilation only before or after
library loading.
.vio
and .vo
files. While
make
insists on building all prerequisites as either
.vio
or .vo
files, Proof General just checks
whether an up-to-date compiled library file is present.
.vo
files and loaded into one Coq instance.
Detailed description of the 4 modes:
no-quick
Compile outdated prerequisites without -quick
, producing .vo
files, but don’t compile prerequisites for which an up-to-date
.vio
file exists. Delete or overwrite outdated .vo
files.
quick-no-vio2vo
Compile outdated prerequisites with -quick
, producing .vio
files, but don’t compile prerequisites for which an up-to-date
.vo
file exists. Delete or overwrite outdated .vio
files.
quick-and-vio2vo
Same as quick-no-vio2vo
, but start vio2vo processes for
missing .vo
files after a certain delay when library
compilation for the current queue region has finished. With this
mode you might see asynchronous errors from vio2vo compilation
while you are processing stuff far below the last require. vio2vo
compilation is done on a subset of the available cores controlled
by option coq-compile-vio2vo-percentage
, Customizing Coq Multiple File Support. When coq-compile-keep-going
is
set, vio2vo compilation is scheduled for those files for which
coqc
compilation was successful.
Warning: This mode does only work when you process require
commands in batches. Slowly single-stepping through require’s
might lead to inconsistency errors when loading some libraries,
see Coq issue #5223. To mitigate this risk, vio2vo compilation
only starts after a certain delay after the last require command
of the current queue region has been processed. This is
controlled by coq-compile-vio2vo-delay
, Customizing Coq Multiple File Support.
ensure-vo
Ensure that all library dependencies are present as .vo
files and delete outdated .vio
files or .vio
files
that are more recent than the corresponding .vo
file. This
setting is the only one that ensures soundness.
The options no-quick
and ensure-vo
are compatible
with Coq 8.4 or older. When Proof General detects such an older
Coq version, it changes the quick compilation mode automatically.
For this to work, the option coq-compile-quick
must only
be set via the customization system or via the menu.
The customization settings for multiple file support of Coq Proof
General are in a separate customization group, the
coq-auto-compile
group. To view all options in this
group do M-x customize-group coq-auto-compile
or select
menu entry Proof-General -> Advanced -> Customize -> Coq ->
Coq Auto Compile -> Coq Auto Compile
.
If non-nil, check dependencies of required modules and compile if necessary.
If non-nil ProofGeneral intercepts "Require" commands and checks if the
required library module and its dependencies are up-to-date. If not, they
are compiled from the sources before the "Require" command is processed.
This option can be set/reset via menu ‘Coq -> Auto Compilation -> Compile Before Require’.
Buffers to save before checking dependencies for compilation.
There are two orthogonal choices: Firstly one can save all or only the coq
buffers, where coq buffers means all buffers in coq mode except the current
buffer. Secondly, Emacs can ask about each such buffer or save all of them
unconditionally.
This makes four permitted values: 'ask-coq
to confirm saving all
modified Coq buffers, 'ask-all
to confirm saving all modified
buffers, 'save-coq
to save all modified Coq buffers without
confirmation and 'save-all
to save all modified buffers without
confirmation.
The following options configure parallel compilation.
Choose the internal compilation method.
When Proof General compiles itself, you have the choice between
two implementations. If this setting is nil, then Proof General
uses the old implementation and compiles everything sequentially
with synchronous job. With this old method Proof General is
locked during compilation. If this setting is t, then the new
method is used and compilation jobs are dispatched in parallel in
the background. The maximal number of parallel compilation jobs
is set with ‘coq-max-background-compilation-jobs
’.
This option can be set/reset via menu ‘Coq -> Auto Compilation -> Compile Parallel In Background’.
The option coq-compile-quick
is described in detail above,
Quick compilation and .vio Files
Continue compilation after the first error as far as possible.
Similar to ‘`make -k’’, with this option enabled, the background
compilation continues after the first error as far as possible.
With this option disabled, background compilation is
immediately stopped after the first error.
This option can be set/reset via menu ‘Coq -> Auto Compilation -> Keep going’.
Maximal number of parallel jobs, if parallel compilation is enabled.
Use the number of available CPU cores if this is set to
'all-cpus
. This variable is the user setting. The value that is
really used is ‘coq--internal-max-jobs
’. Use ‘coq-max-jobs-setter
’
or the customization system to change this variable. Otherwise
your change will have no effect, because ‘coq--internal-max-jobs
’
is not adapted.
Percentage of ‘coq-max-background-vio2vo-percentage
’ for vio2vo jobs.
This setting configures the maximal number of vio2vo background
jobs (if you set ‘coq-compile-quick
’ to 'quick-and-vio2vo
) as
percentage of ‘coq-max-background-compilation-jobs
’.
Delay in seconds for the vio2vo compilation.
This delay helps to avoid running into a library inconsistency
with 'quick-and-vio2vo
, see Coq issue #5223.
Locking ancestors can be disabled with the following option.
If non-nil, lock ancestor module files.
If external compilation is used (via ‘coq-compile-command
’) then
only the direct ancestors are locked. Otherwise all ancestors are
locked when the "Require" command is processed.
The sequential compilation setting supports an external
compilation command (which could be a parallel running
make
). For this set
coq-compile-parallel-in-background
to nil
and
configure the compilation command in coq-compile-command
.
External compilation command. If empty ProofGeneral compiles itself.
If unset (the empty string) ProofGeneral computes the dependencies of
required modules with coqdep and compiles as necessary. This internal
dependency checking does currently not handle ML modules.
If a non-empty string, the denoted command is called to do the dependency checking and compilation. Before executing this command the following keys are substituted as follows:
%p the (physical) directory containing the source of the required module %o the Coq object file in the physical directory that will be loaded %s the Coq source file in the physical directory whose object will be loaded %q the qualified id of the "Require" command %r the source file containing the "Require"
For instance, "make -C %p %o" expands to "make -C bar foo.vo" when module "foo" from directory "bar" is required.
After the substitution the command can be changed in the
minibuffer if ‘coq-confirm-external-compilation
’ is t.
If set let user change and confirm the compilation command.
Otherwise start the external compilation without confirmation.
This option can be set/reset via menu ‘Coq -> Settings -> Confirm External Compilation’.
The preferred way to configure the load path and the mapping of logical library names to physical file path is the Coq project file, Using the Coq project file. Alternatively one can configure these things with the following options.
Non-standard coq library load path.
This list specifies the LoadPath extension for coqdep, coqc and
coqtop. Usually, the elements of this list are strings (for
"-I") or lists of two strings (for "-R" dir path and
"-Q" dir path).
The possible forms of elements of this list correspond to the 4 forms of include options (‘-I’ ‘-Q’ and ‘-R’). An element can be
- A list of the form ‘(’ocamlimport dir)', specifying (in 8.5) a
directory to be added to ocaml path (‘-I’).
- A list of the form ‘(’rec dir path)' (where dir and path are
strings) specifying a directory to be recursively mapped to the
logical path ‘path’ (‘-R dir path’).
- A list of the form ‘(’recnoimport dir path)' (where dir and
path are strings) specifying a directory to be recursively
mapped to the logical path ‘path’ (‘-Q dir path’), but not
imported (modules accessible for import with qualified names
only). Note that -Q dir "" has a special, nonrecursive meaning.
- A list of the form (8.4 only) ‘(’nonrec dir path)', specifying a
directory to be mapped to the logical path 'path'
('-I dir -as path').
For convenience the symbol ‘rec’ can be omitted and entries of the form ‘(dir path)’ are interpreted as ‘(rec dir path)’.
A plain string maps to -Q ... "" in 8.5, and -I ... in 8.4.
Under normal circumstances this list does not need to
contain the coq standard library or "." for the current
directory (see ‘coq-load-path-include-current
’).
warning: if you use coq <= 8.4, the meaning of these options is not the same (-I is for coq path).
If ‘t’ let coqdep search the current directory too.
Should be ‘t’ for normal users. If ‘t’ pass -Q dir "" to coqdep when
processing files in directory "dir" in addition to any entries
in ‘coq-load-path
’.
This setting is only relevant with Coq < 8.5.
During library dependency checking Proof General does not dive
into the Coq standard library or into libraries that are
installed as user contributions. This stems from coqdep
,
which does not output dependencies to these directories.
The internal dependency check can also ignore additional
libraries.
Directories in which ProofGeneral should not compile modules.
List of regular expressions for directories in which ProofGeneral
should not compile modules. If a library file name matches one
of the regular expressions in this list then ProofGeneral does
neither compile this file nor check its dependencies for
compilation. It makes sense to include non-standard coq library
directories here if they are not changed and if they are so big
that dependency checking takes noticeable time. The regular
expressions in here are always matched against the .vo file name,
regardless whether ‘`-quick’’ would be used to compile the file
or not.
Declare ML Module
commands.
Coq allows the user to enter top-level commands while editing a proof script. For example, if the user realizes that the current proof will fail without an additional axiom, he or she can add that axiom to the system while in the middle of the proof. Similarly, the user can nest lemmas, beginning a new lemma while in the middle of an earlier one, and as the lemmas are proved or their proofs aborted they are popped off a stack.
Coq Proof General supports this feature of Coq. Top-level commands entered while in a proof are well backtracked. If new lemmas are started, Coq Proof General lets the user work on the proof of the new lemma, and when the lemma is finished it falls back to the previous one. This is supported to any nesting depth that Coq allows.
Warning! Using Coq commands for navigating inside the different proofs
(Resume
and especially Suspend
) are not supported,
backtracking will break syncronization.
Special note: The old feature that moved nested proofs outside the current proof is disabled.
Another feature that Coq allows is the extension of the grammar of the
proof assistant by new tactic commands. This feature interacts with the
proof script management of Proof General, because Proof General needs to
know when a tactic is called that alters the proof state. When the user
tries to retract across an extended tactic in a script, the algorithm
for calculating how far to undo has a default behavior that is not
always accurate in proof mode: do "Undo
".
Coq Proof General does not currently support dynamic tactic extension in Coq: this is desirable but requires assistance from the Coq core. Instead we provide a way to add tactic and command names in the .emacs file. Four Configurable variables allows to register personal new tactics and commands into four categories:
Back
" to be backtracked;
Undo
" to be backtracked;
We give an example of existing commands that fit each category.
coq-user-state-preserving-commands
: example: "Print
"
coq-user-state-changing-commands
: example: "Require
"
coq-user-state-changing-tactics
: example: "Intro
"
coq-user-state-preserving-tactics
: example: "Idtac
"
This variables are regexp string lists. See their documentations in
emacs (C-h v coq-user...
) for details on how to set them in your
.emacs file.
Here is a simple example:
(setq coq-user-state-changing-commands '("MyHint" "MyRequire")) (setq coq-user-state-preserving-commands '("Show\\s-+Mydata"))
The regexp character sequence \\s-+
means "one or more
whitespaces". See the Emacs documentation of regexp-quote
for the
syntax and semantics. WARNING: you need to restart Emacs to make the
changes to these variables effective.
In case of losing synchronization, the user can use C-c C-z to
move the locked region to the proper position,
(proof-frob-locked-end
, see Escaping script management) or
C-c C-v to re-issue an erroneously back-tracked tactic without
recording it in the script.
Holes are an experimental feature for complex expression editing by filling in templates. It is inspired from other tools, like Pcoq (http://www-sop.inria.fr/lemme/pcoq/index.html). The principle is simple, holes are pieces of text that can be "filled" by various means. The Coq command insertion menu system makes use of the holes system. Almost all holes operations are available in the Holes menu.
Notes: Holes make use of the Emacs abbreviation mechanism, it will
work without problem if you don’t have an abbrev table defined for Coq
in your config files. Use C-h v abbrev-file-name
to see the name
of the abbreviation file.
If you already have such a table it won’t be automatically overwritten
(so that you keep your own abbreviations). But you must read the abbrev
file given in the Proof General sources to be able to use the command
insertion menus. You can do the following to merge your abbreviations
with ProofGeneral’s abbreviations: M-x read-abbrev-file
, then
select the file named coq-abbrev.el
in the
ProofGeneral/coq
directory. At Emacs exit you will be asked if
you want to save abbrevs; answer yes.
Starting with Proof General version 4.2 and Coq version 8.4, Coq Proof General has full support for proof-tree visualization, see Graphical Proof-Tree Visualization. To find out which versions of Prooftree are compatible with this version of Proof General, see Graphical Proof-Tree Visualization or the Prooftree website.
For the visualization to work properly, proofs must be started
with Proof
, which is encouraged practice anyway (see Coq Bug
#2776). Without Proof
you lose the initial proof goal,
possibly having two or more initial goals in the display.
To support Grab Existential Variables
Prooftree can
actually display several graphically independent proof trees in
several layers.
Previous: Holes feature, Up: Coq Proof General [Contents][Index]