diff options
author | Erik Martin-Dorel <erik@martin-dorel.org> | 2019-01-13 12:01:55 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-01-13 12:01:55 +0100 |
commit | 2706e51cd3b1fdb136ca42050d383b8a3a07eab6 (patch) | |
tree | a2dd6e1ce24c4ae4b7709a4876321c3ccf1bcb3a | |
parent | 58cea1b8ffb02bc546ddb56a669d4094390d4809 (diff) | |
parent | 97e8558810c93fd2f8eb7983d7c1ed3cfa7a038b (diff) |
Merge pull request #414 from ProofGeneral/improve-use-package-support
Improve use-package support
-rw-r--r-- | proof-general.el (renamed from pg-init.el) | 32 |
1 files changed, 22 insertions, 10 deletions
diff --git a/pg-init.el b/proof-general.el index 0634de0b..a2f8c6fa 100644 --- a/pg-init.el +++ b/proof-general.el @@ -1,4 +1,4 @@ -;;; pg-init.el --- PG init file for package.el and ELPA compatibility -*- lexical-binding:t; -*- +;;; proof-general.el --- PG init file for package.el and ELPA compatibility -*- lexical-binding: t; -*- ;; This file is part of Proof General. @@ -9,15 +9,14 @@ ;; 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 -;; This program is free software; you can redistribute it and/or modify -;; it under the terms of the GNU General Public License as published by -;; the Free Software Foundation, either version 3 of the License, or -;; (at your option) any later version. +;; This software is free software; you can redistribute it and/or +;; modify it under the terms of the GNU General Public License +;; version 2, as published by the Free Software Foundation. ;; This program is distributed in the hope that it will be useful, ;; but WITHOUT ANY WARRANTY; without even the implied warranty of @@ -29,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. @@ -39,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" @@ -65,5 +77,5 @@ (dolist (dir byte-compile-directories) (add-to-list 'load-path (expand-file-name dir root))))) -(provide 'pg-init) -;;; pg-init.el ends here +(provide 'proof-general) +;;; proof-general.el ends here |