GitHub - hendriktews/proof-tree: proof tree display for Proof General

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 238 Commits
debian		debian
debug		debug
test		test
.gitattributes		.gitattributes
.gitignore		.gitignore
COPYING		COPYING
INSTALL		INSTALL
Makefile.in		Makefile.in
README		README
about_window.ml		about_window.ml
changes.html		changes.html
compatibility		compatibility
configuration.ml		configuration.ml
configure		configure
coq_evar_lexer.mll		coq_evar_lexer.mll
coq_evar_parser.mly		coq_evar_parser.mly
draw_tree.ml		draw_tree.ml
emacs_commands.ml		emacs_commands.ml
evar_types.ml		evar_types.ml
ext_dialog.ml		ext_dialog.ml
gtk_ext.ml		gtk_ext.ml
help_window.ml		help_window.ml
input.ml		input.ml
input.mli		input.mli
main.ml		main.ml
make-deb-package		make-deb-package
make-release		make-release
node_window.ml		node_window.ml
proof_tree.ml		proof_tree.ml
proof_tree.mli		proof_tree.mli
proof_window.ml		proof_window.ml
prooftree.1		prooftree.1
prooftree.opam		prooftree.opam
tree_layers.ml		tree_layers.ml
util.ml		util.ml
version.mli		version.mli
version.txt		version.txt

Repository files navigation

============================================================================
           prooftree --- proof tree display for Proof General
============================================================================


Prooftree is a program for proof tree visualization during interactive
proof development in Proof General. Currently, it only supports Coq. See
http://askra.de/software/prooftree/ for more information.

This version of prooftree requires Proof General later than March 2021 and
Coq version >= 8.11. These versions of Proof General and Coq must be
installed separately.


============================================================================
  USAGE
============================================================================

Start Emacs/Proof General and load any Coq file. Proof display with
prooftree is initially disabled. To enable it, hit the prooftree tool-bar
icon, select menu Proof-General -> Start/Stop Prooftree or type C-c C-d. If
you are inside a proof any of these actions will launch a proof-tree
display for the current proof. Otherwise prooftree will be launched as soon
as you start the next proof. Comprehensive usage information is provided by
the help menu item inside Prooftree and by the Prooftree man page.


============================================================================
CREDITS / CONTACT / COPYRIGHT
============================================================================

Prooftree is more or less a reimplementation of the graphical proof display
of Pvs with a number of enhancements for Coq. The Pvs version is
implemented in Tcl/Tk and controlled directly by the Pvs prover process,
which has some advantages over the prooftree approach.

Please send bug reports, comments, patches, donations to 
Hendrik Tews <[email protected]>

Instructions about adding support for a new proof assistant is contained in
the Proof General Adapting manual.

Prooftree is distributed under GPL version 3.
Copyright (C) 2011 - 2024 Hendrik Tews


============================================================================

Local Variables:
mode: indented-text
fill-column: 75
End: