From 97e8558810c93fd2f8eb7983d7c1ed3cfa7a038b Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sat, 12 Jan 2019 22:02:55 +0100 Subject: 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 --- proof-general.el | 19 ++++++++++++++++--- 1 file 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 +;; 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" -- cgit v1.2.3