9 files changed, 70 insertions, 98 deletions
diff --git a/etc/ProofGeneral.spec b/etc/ProofGeneral.spec
index 2a97e19e..f1d006a7 100644
--- a/etc/ProofGeneral.spec
+++ b/etc/ProofGeneral.spec
@@ -1,6 +1,6 @@
 Summary:	Proof General, Emacs interface for Proof Assistants
 Name:		ProofGeneral
-Version:	4.4.1~pre
+Version:	4.5-git
 Release:	1
 Group:		Text Editors/Integrated Development Environments (IDE)
 License:	GPL
diff --git a/etc/coq/coqdoc-egs.v b/etc/coq/coqdoc-egs.v
deleted file mode 100644
index d79d44e5..00000000
--- a/etc/coq/coqdoc-egs.v
+++ /dev/null
@@ -1,26 +0,0 @@
-(* Some tests/examples of coqdoc regions in Coq files, 
-   used with MMM configuration (ProofGeneral -> Options -> Multiple Modes. *)
-
-
-(** This is a coqdoc plain text region.
-
-    After editing/changing regions in mmm mode, use C-x % C-b to reparse
-*)
-
-
-(** %This is a special case of a \LaTeX{} region recognised by MMM.
-\begin{quote}
-Emacs will be in \texttt{LaTeX} mode when editing this region.
-\end{quote}
- % *)
-
-
-(** #Similarly, this is an HTML region, edited in HTML mode # *)
-
-
-(* Finally, here is some *)
-<<
-verbatim text
->>
-(* in text mode *)
-
diff --git a/etc/development-tips.txt b/etc/development-tips.txt
index 96701285..a6bd0709 100644
--- a/etc/development-tips.txt
+++ b/etc/development-tips.txt
@@ -29,8 +29,11 @@ Top-level forms, or forms that appear at top-level after compilation
 these forms depend on runtime information, e.g., the value of
 proof-assistant symbol (proof-ass), they will produce the wrong result
 (symptom: unbound nil-foobar). Running `proof-ready-for-assistant' can
-be used to avoid this and optimise compilation.  Byte compiler also
-optimises some conditionals that appear constant, be wary.
+be used to avoid this and optimise compilation (CPC 2017-02-25: this
+sounds fishy: this document seems to assume that compilation is done in
+a separate instance of Emacs, but that's not what happens when with
+package.el.  Calling `proof-ready-for-assistant' at compile time will
+tie the rest of that Emacs session to a specific proof assistant).
 
 Finally, the compiler will warn over-eagerly (and ususally spuriously)
 about unknown functions.  Adding extra requires can get these to go
diff --git a/etc/emacsbugs/visiblity-attempt.el b/etc/emacsbugs/visiblity-attempt.el
index ad88799c..b6486116 100644
--- a/etc/emacsbugs/visiblity-attempt.el
+++ b/etc/emacsbugs/visiblity-attempt.el
@@ -1,6 +1,21 @@
-;;;
-;;; === Test area for invisibility ===
-;;;
+;;; visiblity-attempt.el --- Test area for invisibility
+
+;; This file is part of Proof General.
+
+;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
+;; Portions © Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
+;; Portions © Copyright 2001-2017  Pierre Courtieu
+;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
+;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
+;; Portions © Copyright 2015-2017  Clément Pit-Claudel
+
+;;; Commentary:
+;;
+;; Test area for invisibility
+;;
+
+;;; Code:
+
 (defvar vis nil)
 
 (overlay-put (make-overlay 18 22) 'invisible 'smaller)
diff --git a/etc/isar/MMMtests.thy b/etc/isar/MMMtests.thy
deleted file mode 100644
index 994a8ee0..00000000
--- a/etc/isar/MMMtests.thy
+++ /dev/null
@@ -1,40 +0,0 @@
-(* Testing samples for MMM *)
-
-header {* This is edited in LaTeX mode *}
-
-theory MMMtests imports Main begin
-
-text {*
-  This is a test of MMM support.
-  This region is edited in \LaTeX{} mode.
-*}
-
-subsection {* and this one. *}
-
-
-ML {*
-  (* Whereas this region is edited in SML mode.  For that to work, you
-  need to have installed SML mode in your Emacs, otherwise MMM mode
-  won't bother.  See Stefan Monnier's page at
-  http://www.iro.umontreal.ca/~monnier/elisp/. *)
-  
-  fun foo [] = 0
-    | foo (x::xs) = x * foo xs
-*}
-
-ML_val {* (* and this one *) *}
-
-ML_command {* (* and this one *) *}
-
-print_translation {* [] (* and even this one *) *}
-
-text {* 
-  You can enter the text for a MMM region conveniently 
-  using the dedicated insertion commands. For example, I inserted
-  this region by typing \texttt{C-c \% t}  --- see the MMM menu or
-  \texttt{C-c \% h}  for a list of commands.  
-
-  Notice that font locking for different modes tends to interact
-  badly with mode switches between lines.  Best stick to
-  separate lines as in these examples.
-*}
diff --git a/etc/lego/lego-site.el b/etc/lego/lego-site.el
index 55098331..1a31f354 100644
--- a/etc/lego/lego-site.el
+++ b/etc/lego/lego-site.el
@@ -1,8 +1,22 @@
-;;; lego-site.el  Site-specific Emacs support for LEGO
-;;; Copyright (C) 1998 LFCS Edinburgh
+;;; lego-site.el --- Site-specific Emacs support for LEGO
+
+;; This file is part of Proof General.
+
+;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
+;; Portions © Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
+;; Portions © Copyright 2001-2017  Pierre Courtieu
+;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
+;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
+;; Portions © Copyright 2015-2017  Clément Pit-Claudel
+
 ;;; Author: Thomas Kleymann <T.Kleymann@ed.ac.uk>
 ;;; Maintainer: lego@dcs.ed.ac.uk
 
+;;; Commentary:
+;;
+
+;;; Code:
+
 (let ((version (getenv "PROOFGENERAL")))
   (cond ((not version)		;default
 	 (setq load-path
@@ -20,4 +34,4 @@
 	 (load-file "/usr/local/share/elisp/ProofGeneral/generic/proof-site.el"))))
 	 
 
-	 
-\ No newline at end of file
+	 
diff --git a/etc/mmm-install b/etc/mmm-install
deleted file mode 100644
index 41042d23..00000000
--- a/etc/mmm-install
+++ /dev/null
@@ -1,17 +0,0 @@
-#!/bin/sh
-#
-# Install from mmm-mode into PG by copying relevant files
-# Run from inside mmm-mode distrib
-#
-# $Id$
-#
-NOTICES="AUTHORS COPYING FAQ INSTALL NEWS README TODO"
-DOCS="mmm.texinfo version.texi"
-ELISP=*.el
-MMMDIR=~/PG/mmm
-
-rm -f $MMMDIR/*
-cp -p $NOTICES $DOCS $ELISP $MMMDIR
-
-
-
diff --git a/etc/testsuite/pg-pgip-test.el b/etc/testsuite/pg-pgip-test.el
index 9dbfaad7..968c2289 100644
--- a/etc/testsuite/pg-pgip-test.el
+++ b/etc/testsuite/pg-pgip-test.el
@@ -1,6 +1,18 @@
-;; Tests for pg-pgip.el
+;;; Tests for pg-pgip.el
+
+;; This file is part of Proof General.
+
+;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
+;; Portions © Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
+;; Portions © Copyright 2001-2017  Pierre Courtieu
+;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
+;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
+;; Portions © Copyright 2015-2017  Clément Pit-Claudel
+
+;;; Commentary:
 ;;
-;; $Id$
+
+;;; Code:
 
 (pg-clear-test-suite "pg-pgip")
 (pg-set-test-suite   "pg-pgip")
@@ -13,4 +25,4 @@
 
 
 (provide 'pg-pgip-test)
-;; End of `pg-pgip-test.el'
-\ No newline at end of file
+;; End of `pg-pgip-test.el'
diff --git a/etc/testsuite/pg-test.el b/etc/testsuite/pg-test.el
index b8d236a7..2e3c2c10 100644
--- a/etc/testsuite/pg-test.el
+++ b/etc/testsuite/pg-test.el
@@ -1,8 +1,19 @@
-;; pg-test.el -- Simple test framework for Proof General.
-;;
-;; $Id$
+;;; pg-test.el --- Simple test framework for Proof General.
+
+;; This file is part of Proof General.
+
+;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
+;; Portions © Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
+;; Portions © Copyright 2001-2017  Pierre Courtieu
+;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
+;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
+;; Portions © Copyright 2015-2017  Clément Pit-Claudel
+
+;;; Commentary:
 ;;
 
+;;; Code:
+
 (defconst pg-test-buffer "** PG test output **")
 
 (defvar pg-test-total-success-count  0)