aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Erik Martin-Dorel <erik@martin-dorel.org>2019-01-13 12:01:55 +0100
committerGravatar GitHub <noreply@github.com>2019-01-13 12:01:55 +0100
commit2706e51cd3b1fdb136ca42050d383b8a3a07eab6 (patch)
treea2dd6e1ce24c4ae4b7709a4876321c3ccf1bcb3a
parent58cea1b8ffb02bc546ddb56a669d4094390d4809 (diff)
parent97e8558810c93fd2f8eb7983d7c1ed3cfa7a038b (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