Merge pull request #380 from ProofGeneral/prepare-melpa

Prepare PG for MELPA

AUTHORS

@@ -3,12 +3,12 @@ Current Authors/Maintainers:
    Pierre Courtieu     (Coq, lib)
    Erik Martin-Dorel   (Coq, Web site)
    Clément Pit-Claudel (Coq, packaging)
-   Henrik Tews         (Proof Tree)
+   Christophe Raffalli (PhoX)
+   Hendrik Tews        (Proof Tree)
 
 Previous Authors:
 
    David Aspinall     (all)
-   Christoph Raffalli (PhoX)
    Makarius Wenzel    (Isar, generic)
    Stefan Berghofer   (Isar)
    Paul Callaghan     (Plastic, Lego)

CHANGES

@@ -4,7 +4,7 @@ This is a summary of main changes.  For details, please see
 the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG
 and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac
 
-* Changes of Proof General 4.4.1 from Proof General 4.4
+* Changes of Proof General 4.5 from Proof General 4.4
 
 ** Generic changes
 

Makefile.devel

@@ -91,8 +91,8 @@ DEVELOPERS=\
 # The prereltag.txt is kept as a record in the distrib area
 # of the current pre-release version (currently not used explicitly
 # anywhere for web pages/whatever).
-PRERELEASE_PREFIX=4\.4\.1~pre
-PRERELEASE_TAG=4.4.1~pre
+PRERELEASE_PREFIX=4\.5-git
+PRERELEASE_TAG=4.5-git
 ### Formerly: PRERELEASE_TAG=4.4pre$(shell date "+%y%m%d")
 PREREL_TAG_FILE=prereltag.txt
 

Makefile.travis

@@ -1,4 +1,4 @@
-VERSIONS = 24.1 24.2 24.3 24.4 24.5 25.1 25.2 25.3
+VERSIONS = 24.3 24.4 24.5 25.1 25.2 25.3
 STABLE_TARGETS = $(addprefix prepare-emacs-,$(VERSIONS))
 
 .PHONY: prepare-emacs-24 prepare-emacs-git $(STABLE_TARGETS) \

README.md

@@ -8,7 +8,7 @@ Proof General is a generic Emacs interface for proof assistants.
 The aim of the Proof General project is to provide a powerful, generic
 environment for using interactive proof assistants.
 
-This is version 4.4.1~pre of Proof General.
+This is version 4.5-git of Proof General.
 
 ## About Proof General branches
 

coq/coq-abbrev.el

@@ -69,7 +69,7 @@
 ;;; The abbrev table built from keywords tables
 ;#s and @{..} are replaced by holes by holes-abbrev-complete
 (defun coq-install-abbrevs ()
-  "install default abbrev table for coq if no other already is."
+  "Install default abbrev table for coq if no other already is."
   (if (boundp 'coq-mode-abbrev-table)
       ;; da: this test will always fail.  Assume bound-->non-empty
       ;; (not (equal coq-mode-abbrev-table (make-abbrev-table))))
@@ -353,9 +353,11 @@ It was constructed with `proof-defstringset-fn'.")
      ["Compile" coq-Compile t]))))
 
 (setq-default coq-help-menu-entries
-  '(["help on setting prog name persistently for a file" 
+  '(["help on setting prog name persistently for a file"
      coq-local-vars-list-show-doc t]))
 
 (setq-default coq-other-buffers-menu-entries coq-menu-common-entries)
 
 (provide 'coq-abbrev)
+
+;;; coq-abbrev.el ends here

coq/coq-autotest.el

@@ -97,3 +97,7 @@
   (pg-autotest timetaken 'total)
 
   (pg-autotest exit))
+
+(provide 'coq-autotest)
+
+;;; coq-autotest.el ends here

coq/coq-db.el

@@ -78,10 +78,10 @@ new keyword to colorize.")
 
 (defun coq-insert-from-db (db prompt &optional alwaysjump)
   "Ask for a keyword, with completion on keyword database DB and insert.
-Insert corresponding string with holes at point. If an insertion
-function is present for the keyword, call it instead. see
-`coq-syntax-db' for DB structure. If ALWAYSJUMP is non nil, jump
-to the first hole even if more than one."
+Insert corresponding string with holes at point.  If an insertion
+function is present for the keyword, call it instead. See
+`coq-syntax-db' for DB structure.  If ALWAYSJUMP is non nil, jump to
+the first hole even if more than one."
   (let* ((tac (completing-read (concat prompt " (TAB for completion): ")
 			       db nil nil))
 	 (infos (cddr (assoc tac db)))
@@ -96,7 +96,7 @@ to the first hole even if more than one."
 
 
 (defun coq-build-command-from-db (db prompt &optional preformatquery)
-  "Ask for a keyword, with completion on keyword database DB and send to coq.
+  "Ask for a keyword, with completion on keyword database DB and send to Coq.
 See `coq-syntax-db' for DB structure."
   ;; Next invocation of minibuffer (read-string below) will first recursively
   ;; ask for a command in db and expand it with holes. This way the cursor will
@@ -142,7 +142,7 @@ regexp.  See `coq-syntax-db' for DB structure."
 ;	     (color (concat "\\_<" (nth 4 hd) "\\_>")))       ; colorization string
 	;; TODO delete doublons
 	(when (and color (or (not filter) (funcall filter hd)))
-	  (setq res 
+	  (setq res
 		(nconc res (list
 			    (concat "\\_<" color "\\_>")))))
 	(setq l tl)))
@@ -204,8 +204,8 @@ Used by `coq-build-menu-from-db', which you should probably use instead.  See
 	  (let ((menu-entry
 		 (vector
 		  ;; menu entry label
-		  (concat menu 
-			  (if (not abbrev) "" 
+		  (concat menu
+			  (if (not abbrev) ""
 			    (concat spaces "(" abbrev keybind-abbrev ")")))
 		  ;;insertion function if present otherwise insert completion
 		  (if insertfn insertfn `(holes-insert-and-expand ,complt))
@@ -254,8 +254,7 @@ structure."
     res))
 
 (defcustom coq-holes-minor-mode t
-  "*Whether to apply holes minor mode (see `holes-show-doc') in
-  coq mode."
+  "*Whether to apply holes minor mode (see `holes-show-doc') in coq mode."
   :type 'boolean
   :group 'coq)
 
@@ -298,7 +297,7 @@ See `coq-syntax-db' for DB structure."
   "Face for names of closing tactics in proof scripts."
   :group 'proof-faces)
 
-;;A face for cheating tactics 
+;;A face for cheating tactics
 ;; We use :box in addition to :background because box remains visible in
 ;; locked-region. :reverse-video is another solution.
 (defface coq-cheat-face