aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Erik Martin-Dorel <erik@martin-dorel.org>2019-01-12 22:02:55 +0100
committerGravatar Erik Martin-Dorel <erik@martin-dorel.org>2019-01-13 02:47:43 +0100
commit97e8558810c93fd2f8eb7983d7c1ed3cfa7a038b (patch)
treea2dd6e1ce24c4ae4b7709a4876321c3ccf1bcb3a
parentbeebf0f144a04190c0f0910860f603a14f937b6b (diff)
Update the commentary section in proof-general.el
as this text should document the whole package and will be shown at http://www.melpa.org/#/proof-general href: https://github.com/ProofGeneral/PG/issues/198#issuecomment-419741803
-rw-r--r--proof-general.el19
1 files changed, 16 insertions, 3 deletions
diff --git a/proof-general.el b/proof-general.el
index fac8f5ac..a2f8c6fa 100644
--- a/proof-general.el
+++ b/proof-general.el
@@ -9,7 +9,7 @@
;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
;; Portions © Copyright 2015-2017 Clément Pit-Claudel
-;; Author: Clément Pit-Claudel <clement.pitclaudel@live.com>
+;; Authors: (see the AUTHORS file distributed along the sources)
;; URL: https://proofgeneral.github.io/
;; Package-Requires: ((emacs "24.3"))
;; Version: 4.5-git
@@ -28,6 +28,21 @@
;;; Commentary:
;;
+;; Proof General is a generic Emacs interface for proof assistants
+;; (also known as interactive theorem provers).
+;;
+;; It is supplied ready to use for the proof assistants Coq,
+;; EasyCrypt, and PhoX.
+;;
+;; See https://proofgeneral.github.io/ for installation instructions
+;; and online documentation. Or browse the accompanying info manual:
+;; (info-display-manual "ProofGeneral")
+;;
+;; Regarding the Coq proof assistant, you may be interested in the
+;; company-coq extension of ProofGeneral (also available in MELPA).
+
+;;; Code:
+
;; Proof General's initialization code (in generic/proof-site) is relatively
;; complex, in part because it was written before package.el existed, and in
;; part because package.el still doesn't look for autoloads in subdirectories.
@@ -38,8 +53,6 @@
;; * Loading a minimal PG setup on startup (not all of Proof General, of course;
;; mostly mode hooks and autoloads).
-;;; Code:
-
;;;###autoload
(if t (require 'proof-site
(expand-file-name "generic/proof-site"