diff options
author | Erik Martin-Dorel <erik@martin-dorel.org> | 2019-01-12 22:02:55 +0100 |
---|---|---|
committer | Erik Martin-Dorel <erik@martin-dorel.org> | 2019-01-13 02:47:43 +0100 |
commit | 97e8558810c93fd2f8eb7983d7c1ed3cfa7a038b (patch) | |
tree | a2dd6e1ce24c4ae4b7709a4876321c3ccf1bcb3a | |
parent | beebf0f144a04190c0f0910860f603a14f937b6b (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.el | 19 |
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" |