aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorThomas Kleymann1998-12-15 16:01:38 +0000
committerThomas Kleymann1998-12-15 16:01:38 +0000
commita8d8b5acb8bec7ab8aa5abdec8d92b171092ba07 (patch)
tree0b26b455d1c80a367c580a0b152bedfe9b3cb436 /doc
parentb6aef44fd311f42333aae829c2d70d392e3d8848 (diff)
*** empty log message ***
Diffstat (limited to 'doc')
-rw-r--r--doc/ProofGeneral.texi15
1 files changed, 12 insertions, 3 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 8556af29..874ac746 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1895,6 +1895,14 @@ Intros
Apply
@end table
+Sorry, there is currently very little specific documentation written for
+Coq Proof General. If any Coq user would like to contribute, please send
+a message to @code{proofgen@@dcs.ed.ac.uk}.
+
+Type @kbd{C-h C-m} to get a list of all Coq specific commands and
+browse the customize menus to find out what customization
+options there are for Coq.
+
@c
@c CHAPTER: Isabelle Proof General
@c
@@ -3408,9 +3416,10 @@ is being maintained by David Aspinall @i{<isabelle@@dcs.ed.ac.uk>}.
The generic base for Proof General was developed by Kleymann, Sequeira,
Goguen and Aspinall (in order of appearance). It follows some of the
-ideas used in Project CROAP. The Proof General project was initiated in
-1994 and coordinated until October 1998 by Thomas Kleymann. Since
-October 1998, David Aspinall is in charge of Proof General.
+ideas used in Project @uref{http://www.inria.fr/croap/,CROAP}. The Proof
+General project was initiated in 1994 and coordinated until October 1998
+by Thomas Kleymann. Since October 1998, David Aspinall is in charge of
+Proof General.
An early version of this manual was prepared by Dilip Sequeira. The
present version was written by David Aspinall and Thomas Kleymann.