Merge pull request #194 from ProofGeneral/update-headers

Update copyright messages and improve the header of elisp files.

73 files changed, 1001 insertions, 378 deletions

diff --git a/acl2/acl2.el b/acl2/acl2.el
index 4f023217..cf9f521c 100644
--- a/acl2/acl2.el
+++ b/acl2/acl2.el
@@ -1,15 +1,25 @@
-;; acl2.el   Basic Proof General instance for ACL2
-;;
-;; Copyright (C) 2000 LFCS Edinburgh.
+;;; acl2.el --- Basic Proof General instance for ACL2
+
+;; 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
+
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
+
 ;; Author:    David Aspinall <David.Aspinall@ed.ac.uk>
-;;
-;; $Id$
+
+;;; Commentary:
 ;;
 ;; Needs improvement!
 ;;
 ;; See the README file in this directory for information.
 
+;;; Code:
 
 (require 'proof-easy-config)            ; easy configure mechanism
 (require 'proof-syntax)			; functions for making regexps
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 3a750472..5a555df5 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -1,10 +1,23 @@
 ;;; coq-abbrev.el --- coq abbrev table and menus for ProofGeneral mode
-;;
-;; Copyright (C) 1994-2009 LFCS Edinburgh.
+
+;; 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
+
 ;; Authors: Healfdene Goguen, Pierre Courtieu
+;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
+
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
+
+;;; Commentary:
 ;;
-;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
+
+;;; Code:
 
 (require 'proof)
 (require 'coq-syntax)
diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el
index e3c4b978..9126c2ae 100644
--- a/coq/coq-autotest.el
+++ b/coq/coq-autotest.el
@@ -1,9 +1,20 @@
-;; coq-autotest.el: tests of Coq Proof General (in progress).
+;;; coq-autotest.el --- tests of Coq Proof General (in progress).
+
+;; 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:
 ;;
 ;; You can run these by issuing "make test.coq" in PG home dir.
 ;;
-;; $Id$
-;;
+
+;;; Code:
 
 (eval-when-compile
   (require 'cl))
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index f96b07da..c94cd8b7 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -1,17 +1,26 @@
-;; coq-compile-common.el --- common part of compilation feature
-;; Copyright (C) 1994-2012 LFCS Edinburgh.
+;;; coq-compile-common.el --- common part of compilation feature
+
+;; 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
+
 ;; Authors: Hendrik Tews
-;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Maintainer: Hendrik Tews <hendrik@askra.de>
-;;
-;; $Id$
-;;
+
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
+
 ;;; Commentary:
 ;;
 ;; This file holds constants, options and some general functions for
 ;; the compilation feature.
 ;;
 
+;;; Code:
 
 (require 'proof-shell)
 (require 'coq-system)
diff --git a/coq/coq-db.el b/coq/coq-db.el
index 13badf56..dd9020d8 100644
--- a/coq/coq-db.el
+++ b/coq/coq-db.el
@@ -1,9 +1,18 @@
-;;; coq-db.el --- coq keywords database utility functions
-;;
+;;; coq-db.el --- coq keywords database utility functions -*- coding: utf-8; -*-
+
+;; 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: Pierre Courtieu <courtieu@lri.fr>
+
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;;
+
 ;;; Commentary:
 ;;
 ;; We store all information on keywords (tactics or command) in big
@@ -284,7 +293,7 @@ See `coq-syntax-db' for DB structure."
 (defface coq-solve-tactics-face
   (proof-face-specs
    (:foreground "red") ; pour les fonds clairs
-   (:foreground "red1") ; pour les fond foncés
+   (:foreground "red1") ; pour les fonds foncés
    ()) ; pour le noir et blanc
   "Face for names of closing tactics in proof scripts."
   :group 'proof-faces)
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index b6b8c18d..405cbb46 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -1,9 +1,17 @@
 ;;; coq-indent.el --- indentation for Coq
-;;
-;; Copyright (C) 2004-2006 LFCS Edinburgh.
+
+;; 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
+
 ;; Authors: Pierre Courtieu
 ;; Maintainer: Pierre Courtieu <courtieu@lri.fr>
-;;
+
 ;; Commentary:
 ;; 
 ;; Indentation for Coq.
diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el
index 50a1f626..a097043a 100644
--- a/coq/coq-local-vars.el
+++ b/coq/coq-local-vars.el
@@ -1,14 +1,22 @@
 ;;; coq-local-vars.el --- local variable list tools for coq
-;;
-;; Copyright (C) 2006-2008 LFCS Edinburgh.
+
+;; 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
+
 ;; Authors: Pierre Courtieu
 ;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
-;;
-;; $Id$
-;;
+
 ;;; Commentary:
 ;;
 
+;;; Code:
+
 (require 'local-vars-list)              ; in lib directory
 
 (eval-when-compile
@@ -19,7 +27,6 @@
   (defvar coq-load-path))
 
 
-;;; Code:
 (defconst coq-local-vars-doc nil
   "Documentation-only variable.
 
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index 1580febd..17fe12d5 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -1,11 +1,19 @@
-;; coq-par-compile.el --- parallel compilation of required modules
-;; Copyright (C) 1994-2012 LFCS Edinburgh.
+;;; coq-par-compile.el --- parallel compilation of required modules
+
+;; 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
+
 ;; Authors: Hendrik Tews
-;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Maintainer: Hendrik Tews <hendrik@askra.de>
-;;
-;; $Id$
-;;
+
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
+
 ;;; Commentary:
 ;;
 ;; This file implements compilation of required modules. The
@@ -24,6 +32,8 @@
 ;; changing compilers, all compilation jobs must be terminated.  This is
 ;; consistent with the fact that the _CoqProject file is not reparsed.
 
+;;; Code:
+
 (eval-when-compile
   (require 'proof-compat))
 
diff --git a/coq/coq-par-test.el b/coq/coq-par-test.el
index f60baacf..8e83d1d4 100644
--- a/coq/coq-par-test.el
+++ b/coq/coq-par-test.el
@@ -1,9 +1,19 @@
-;; coq-par-test.el --- tests for parallel compilation
-;; Copyright (C) 2016 Hendrik Tews
+;;; coq-par-test.el --- tests for parallel compilation
+
+;; 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
+
 ;; Authors: Hendrik Tews
-;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Maintainer: Hendrik Tews <hendrik@askra.de>
-;;
+
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
+
 ;;; Commentary:
 ;;
 ;; This file file contains tests for `coq-par-job-needs-compilation'.
@@ -18,6 +28,7 @@
 ;;
 ;; - integrate into PG build and test(?) system
 
+;;; Code:
 
 (require 'coq-par-compile)
 
diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el
index bf492f82..90bd3c3d 100644
--- a/coq/coq-seq-compile.el
+++ b/coq/coq-seq-compile.el
@@ -1,11 +1,19 @@
-;; coq-seq-compile.el --- sequential compilation of required modules
-;; Copyright (C) 1994-2012 LFCS Edinburgh.
+;;; coq-seq-compile.el --- sequential compilation of required modules
+
+;; 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
+
 ;; Authors: Hendrik Tews
-;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Maintainer: Hendrik Tews <hendrik@askra.de>
-;;
-;; $Id$
-;;
+
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
+
 ;;; Commentary:
 ;;
 ;; This file implements compilation of required modules. The
@@ -14,6 +22,7 @@
 ;; proof-action-list and compiles one module after the other.
 ;;
 
+;;; Code:
 
 (eval-when-compile
   (require 'proof-compat))
diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 4565d86c..2b5e59e9 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -1,10 +1,18 @@
 ;;; coq-smie.el --- SMIE lexer, grammar, and indent rules for Coq
 
-;; Copyright (C) 2014  Free Software Foundation, Inc
+;; 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
 
 ;; Authors: Pierre Courtieu
 ;;          Stefan Monnier
 ;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
+
 ;; License:     GPLv3+ (GNU GENERAL PUBLIC LICENSE version 3 or later)
 
 ;;; Commentary:
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 5b55126c..63d44666 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1,10 +1,23 @@
-;; coq-syntax.el Font lock expressions for Coq
-;; Copyright (C) 1997-2007, 2009 LFCS Edinburgh.
+;;; coq-syntax.el --- Font lock expressions for Coq
+
+;; 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
+
 ;; Authors: Thomas Kleymann, Healfdene Goguen, Pierre Courtieu
-;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
 
-;; coq-syntax.el,v 11.13 2013/07/10 14:59:08 pier Exp
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
+
+;;; Commentary:
+;;
+
+;;; Code:
 
 (require 'proof-syntax)
 (require 'proof-utils)                  ; proof-locate-executable
diff --git a/coq/coq-system.el b/coq/coq-system.el
index 8da4ea23..14da9f17 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -1,9 +1,18 @@
-;; coq-system.el --- common part of compilation feature
-;; Copyright (C) 2015 LFCS Edinburgh.
+;;; coq-system.el --- common part of compilation feature
+
+;; 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
+
 ;; Authors: Hendrik Tews, Pierre Courtieu
-;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Maintainer: Pierre.Courtieu<Pierre.Courtieu@cnam.fr>
-;;
+
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 
 ;;; Commentary:
 ;;
@@ -12,6 +21,8 @@
 ;; support for older versions of coq.
 ;;
 
+;;; Code:
+
 (require 'proof)
 
 (eval-when-compile
diff --git a/coq/coq-unicode-tokens.el b/coq/coq-unicode-tokens.el
index faa02458..5f2cd0c6 100644
--- a/coq/coq-unicode-tokens.el
+++ b/coq/coq-unicode-tokens.el
@@ -1,8 +1,17 @@
-;;; -*- coding: utf-8; -*-
-;; coq-unicode-tokens.el --- (No) Tokens for Unicode Tokens package
-;;
-;; Copyright(C) 2008, 2009 David Aspinall / LFCS Edinburgh
+;;; coq-unicode-tokens.el --- (No) Tokens for Unicode Tokens package -*- coding: utf-8; -*-
+
+;; 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:    David Aspinall <David.Aspinall@ed.ac.uk>
+
+;;; Commentary:
 ;;
 ;; This file is loaded by `proof-unicode-tokens.el'.
 ;;
diff --git a/coq/coq.el b/coq/coq.el
index 793c59a0..e630a561 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1,12 +1,23 @@
-;; coq.el --- Major mode for Coq proof assistant  -*- coding: utf-8 -*-
-;; Copyright (C) 1994-2009 LFCS Edinburgh.
+;;; coq.el --- Major mode for Coq proof assistant  -*- coding: utf-8 -*-
+
+;; 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
+
 ;; Authors: Healfdene Goguen, Pierre Courtieu
-;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
-;;
-;; $Id$
 
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
+
+;;; Commentary:
+;;
 
+;;; Code:
 
 (eval-when-compile
   (require 'cl)
diff --git a/doc/docstring-magic.el b/doc/docstring-magic.el
index 1d074d8d..614b56e2 100644
--- a/doc/docstring-magic.el
+++ b/doc/docstring-magic.el
@@ -1,13 +1,24 @@
-;; doc/docstring-magic.el  -- hack for using texi-docstring-magic.
-;;
-;; Copyright (C) 1998 LFCS Edinburgh. 
+;;; doc/docstring-magic.el --- hack for using texi-docstring-magic.
+
+;; 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: David Aspinall
 ;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
+
+;;; Commentary:
 ;;
 ;; Ensure that non-compiled versions of everything are loaded.
 ;;
-;; $Id$
-;;
+
+;;; Code:
+
 (setq load-path
       (append '("../generic/") load-path))
 (load "proof-site.el")
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/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/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)
diff --git a/generic/pg-assoc.el b/generic/pg-assoc.el
index a8a52099..714429b7 100644
--- a/generic/pg-assoc.el
+++ b/generic/pg-assoc.el
@@ -1,12 +1,19 @@
 ;;; pg-assoc.el --- Functions for associated buffers
-;;
-;; Copyright (C) 1994-2008, 2010 LFCS Edinburgh.
+
+;; 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
+
 ;; Authors:   David Aspinall, Yves Bertot, Healfdene Goguen,
 ;;            Thomas Kleymann and Dilip Sequeira
+
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
+
 ;;; Commentary:
 ;;
 ;; Defines an empty mode inherited by modes of the associated buffers.
diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el
index 8dfee09d..bc3ab9c5 100644
--- a/generic/pg-autotest.el
+++ b/generic/pg-autotest.el
@@ -1,10 +1,18 @@
 ;;; pg-autotest.el --- Simple testing framework for Proof General
-;;
-;; Copyright (C) 2005, 2009-11 LFCS Edinburgh, David Aspinall.
+
+;; 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
+
 ;; Authors:   David Aspinall
-;;
+
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
-;;
+
 ;;; Commentary:
 ;;
 ;; Support for running a series of scripted UI tests.
@@ -14,8 +22,8 @@
 ;; -- add macros for defining test suites
 ;; -- add more precise functional tests to check results
 ;; -- add negative tests
-;;
-;; $Id$
+
+;;; Code:
 
 (require 'proof-splash)
 (setq proof-splash-enable nil)		; prevent splash when testing
diff --git a/generic/pg-custom.el b/generic/pg-custom.el
index 0956f970..8a7bb793 100644
--- a/generic/pg-custom.el
+++ b/generic/pg-custom.el
@@ -1,11 +1,18 @@
 ;;; pg-custom.el --- Proof General per-prover settings
-;;
-;; Copyright (C) 2008, 2010 LFCS Edinburgh.
+
+;; 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:      David Aspinall <David.Aspinall@ed.ac.uk> and others
+
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
+
 ;;; Commentary:
 ;;
 ;; Prover specific settings and user options.
diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index 5270ae3d..c35f0f29 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -1,12 +1,18 @@
-;; pg-goals.el ---  Proof General goals buffer mode.
-;;
-;; Copyright (C) 1994-2009 LFCS, University of Edinburgh.
+;;; pg-goals.el --- Proof General goals buffer mode.
+
+;; 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
+
 ;; Authors:   David Aspinall, Yves Bertot, Healfdene Goguen,
 ;;            Thomas Kleymann and Dilip Sequeira
+
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
 
 ;;; Commentary:
 
diff --git a/generic/pg-movie.el b/generic/pg-movie.el
index 03ea5497..ba641c20 100644
--- a/generic/pg-movie.el
+++ b/generic/pg-movie.el
@@ -1,11 +1,18 @@
 ;;; pg-movie.el --- Export a processed script buffer for external replay
-;;
-;; Copyright (C) 2010 LFCS Edinburgh.
+
+;; 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:      David Aspinall <David.Aspinall@ed.ac.uk> and others
+
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
+
 ;;; Commentary:
 ;;
 ;; Given a processed proof script, write out an XML file that
diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el
index d7bb1bf3..9792dfd0 100644
--- a/generic/pg-pamacs.el
+++ b/generic/pg-pamacs.el
@@ -1,8 +1,16 @@
 ;;; pg-pamacs.el --- Macros for per-proof assistant configuration
-;;
-;; Copyright (C) 2010, 2011  LFCS Edinburgh, David Aspinall.
-;;
+
+;; 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: David Aspinall <da@longitude>
+
 ;; Keywords: internal
 
 ;;; Commentary:
@@ -24,14 +32,13 @@
 ;;
 ;; (proof-ass name)  or (proof-assistant-name)
 ;;
-;;
+
+;;; Code:
 
 (require 'proof-site)			; proof-assitant-symbol
 (require 'proof-compat)			; pg-custom-undeclare-variable
 (require 'proof-autoloads)		; proof-debug
 
-;;; Code:
-
 (defmacro deflocal (var value &optional docstring)
   "Define a buffer local variable VAR with default value VALUE."
  `(progn
diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el
index cd9dac2a..997f8bb1 100644
--- a/generic/pg-pgip.el
+++ b/generic/pg-pgip.el
@@ -1,10 +1,19 @@
-;; pg-pgip.el --- PGIP manipulation for Proof General
-;;
-;; Copyright (C) 2000-2002, 2010 LFCS Edinburgh.
+;;; pg-pgip.el --- PGIP manipulation 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
+
 ;; Author:   David Aspinall <David.Aspinall@ed.ac.uk>
+
 ;; License:  GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
+
+;;; Commentary:
 ;;
 ;; STATUS: Experimental
 ;;
@@ -23,10 +32,7 @@
 ;; -- support fully native PGIP mode
 ;;
 
-
-;;; Commentary:
-;;
-
+;;; Code:
 (require 'cl)				; incf
 (require 'pg-xml)			;
 
@@ -35,7 +41,6 @@
 (declare-function proof-segment-up-to "proof-script") 
 (declare-function proof-insert-pbp-command "proof-script")
 
-;;; Code:
 (defalias 'pg-pgip-debug   'proof-debug)
 (defalias 'pg-pgip-error   'error)
 (defalias 'pg-pgip-warning 'pg-internal-warning)
diff --git a/generic/pg-response.el b/generic/pg-response.el
index 8b6a413a..d89d3c0b 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -1,12 +1,19 @@
-;; pg-response.el --- Proof General response buffer mode.
-;;
-;; Copyright (C) 1994-2010 LFCS Edinburgh.
+;;; pg-response.el --- Proof General response buffer mode.
+
+;; 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
+
 ;; Authors:   David Aspinall, Healfdene Goguen,
 ;;		Thomas Kleymann and Dilip Sequeira
+
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; pg-response.el,v 12.10 2012/09/25 09:44:18 pier Exp
-;;
+
 ;;; Commentary:
 ;;
 ;; This mode is used for the response buffer proper, and
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 11a731fb..21d9479d 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -1,13 +1,18 @@
 ;;; pg-user.el --- User level commands for Proof General
-;;
-;; Copyright (C) 2000-2010 LFCS Edinburgh.
-;; Copyright (c) 2010 Erik Martin-Dorel, ENS de Lyon (pg-protected-undo).
+
+;; 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:     David Aspinall and others
+
 ;; License:    GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
-;;
+
 ;;; Commentary:
 ;;
 ;; This file defines some user-level commands.  Most of them
diff --git a/generic/pg-vars.el b/generic/pg-vars.el
index 8d93a60b..546c955e 100644
--- a/generic/pg-vars.el
+++ b/generic/pg-vars.el
@@ -1,11 +1,18 @@
 ;;; pg-vars.el --- Proof General global variables
-;;
-;; Copyright (C) 2008, 2010 LFCS Edinburgh.
+
+;; 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:      David Aspinall <David.Aspinall@ed.ac.uk> and others
+
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
+
 ;;; Commentary:
 ;;
 ;; Global variables used in several files.
diff --git a/generic/pg-xml.el b/generic/pg-xml.el
index 79d15b55..5de8095d 100644
--- a/generic/pg-xml.el
+++ b/generic/pg-xml.el
@@ -1,14 +1,25 @@
-;; pg-xml.el --- XML functions for Proof General
-;;
-;; Copyright (C) 2000-2002 LFCS Edinburgh.
+;;; pg-xml.el --- XML functions 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
+
 ;; Author:     David Aspinall <David.Aspinall@ed.ac.uk>
+
 ;; License:    GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
+
+;;; Commentary:
 ;;
 ;; XML functions for Proof General.
 ;;
 
+;;; Code:
+
 (require 'cl)
 
 (require 'xml)
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index 67287511..5cd83ddd 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -1,5 +1,17 @@
 ;;; proof-autoloads.el --- automatically extracted autoloads
+
+;; 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:
 
 (if (featurep 'proof-autoloads) (error "Already loaded"))
diff --git a/generic/proof-auxmodes.el b/generic/proof-auxmodes.el
index aa6ddd23..d3ccf41e 100644
--- a/generic/proof-auxmodes.el
+++ b/generic/proof-auxmodes.el
@@ -1,7 +1,16 @@
 ;;; proof-auxmodes.el --- Arrange for auxiliary modes to be loaded when required
-;;
-;; Copyright (C) 2008, 2010 David Aspinall / LFCS Edinburgh
+
+;; 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:    David Aspinall <David.Aspinall@ed.ac.uk>
+
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 
 ;;; Commentary:
@@ -10,10 +19,10 @@
 ;; loading of their main defining files and the possibility to disable them.
 ;;
 
-(require 'proof-utils)			; proof-ass, proof-eval...
-
 ;;; Code:
 
+(require 'proof-utils)			; proof-ass, proof-eval...
+
 ;;
 ;; Maths menu
 ;;
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 8bb40634..bd5ca611 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1,11 +1,18 @@
 ;;; proof-config.el --- Proof General configuration for proof assistant
-;;
-;; Copyright (C) 1998-2010 LFCS Edinburgh.
+
+;; 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:      David Aspinall <David.Aspinall@ed.ac.uk> and others
+
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
+
 ;;; Commentary:
 ;;
 ;; This file declares all prover-specific configuration variables for
diff --git a/generic/proof-depends.el b/generic/proof-depends.el
index c55df53d..74332c71 100644
--- a/generic/proof-depends.el
+++ b/generic/proof-depends.el
@@ -1,21 +1,28 @@
 ;;; proof-depends.el --- Theorem-theorem and theorem-definition dependencies
-;;
-;; Copyright (C) 2000-2004, 2010 University of Edinburgh.
+
+;; 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
+
 ;; Authors:      David Aspinall <David.Aspinall@ed.ac.uk>
 ;;	         Earlier version by Fiona McNeil.
+
 ;; License:      GPL (GNU GENERAL PUBLIC LICENSE)
-;; Status:       Experimental code
+
+;;; Commentary:
 ;;
-;; $Id$
+;; Status:       Experimental code
 ;;
-;;; Commentary:
-;; 
 ;; Based on Fiona McNeill's MSc project on analysing dependencies
 ;; within proofs.  Code rewritten by David Aspinall.
 ;;
 
-
-
+;;; Code:
 (require 'cl)
 (require 'span)
 (require 'pg-vars)
@@ -34,9 +41,6 @@ A list of lists; the first element of each list is a file-name, the
 second element a list of all the def names in that file.
 i.e.: ((file-name-1 (def1 def2 def3)) (file-name-2 (def1 def2 def3)))")
 
-
-;;; Code:
-
 ;; Utility functions
 
 (defun proof-depends-module-name-for-buffer ()
diff --git a/generic/proof-easy-config.el b/generic/proof-easy-config.el
index da3b9c7f..59fa03e5 100644
--- a/generic/proof-easy-config.el
+++ b/generic/proof-easy-config.el
@@ -1,16 +1,27 @@
-;; proof-easy-config.el    Easy configuration for Proof General
-;;
-;; Copyright (C) 1999-2002  David Aspinall / LFCS.
+;;; proof-easy-config.el --- Easy configuration 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
+
 ;; Author:    David Aspinall <David.Aspinall@ed.ac.uk>
+
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
+
+;;; Commentary:
 ;;
 ;; Future versions might copy settings instead; consider how best to
 ;; interface with customization mechanism so a new prover can be
 ;; configured by editing inside custom buffers.
 ;;
 
+;;; Code:
+
 (require 'proof-site)			; proof-assistant, proof-assistant-symbol
 (require 'proof-auxmodes)		; make sure extra modes available
 
diff --git a/generic/proof-faces.el b/generic/proof-faces.el
index 0eafc075..92609d47 100644
--- a/generic/proof-faces.el
+++ b/generic/proof-faces.el
@@ -1,11 +1,18 @@
 ;;; proof-faces.el --- Faces for Proof General
-;;
-;; Copyright (C) 2009 LFCS Edinburgh.
+
+;; 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:      David Aspinall <David.Aspinall@ed.ac.uk> and others
+
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
+
 ;;; Commentary:
 ;;
 ;; In an ideal world, faces should work sensibly:
diff --git a/generic/proof-indent.el b/generic/proof-indent.el
index 2ff6cf69..24da2059 100644
--- a/generic/proof-indent.el
+++ b/generic/proof-indent.el
@@ -1,21 +1,27 @@
 ;;; proof-indent.el --- Generic indentation for proof assistants
-;;
+
+;; 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
+
 ;; Authors:	   Markus Wenzel, David Aspinall
-;; License:        GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
 
+;; License:        GPL (GNU GENERAL PUBLIC LICENSE)
 
 ;;; Commentary:
 ;; 
 
+;;; Code:
 (require 'proof-config)			; config variables
 (require 'proof-utils)			; proof-ass
 (require 'proof-syntax)			; p-looking-at-safe, p-re-search
 (require 'proof-autoloads)		; p-locked-end
 
-;;; Code:
 (defun proof-indent-indent ()
   "Determine indentation caused by syntax element at current point."
   (cond
diff --git a/generic/proof-maths-menu.el b/generic/proof-maths-menu.el
index 57fafa98..b1155557 100644
--- a/generic/proof-maths-menu.el
+++ b/generic/proof-maths-menu.el
@@ -1,16 +1,22 @@
 ;;; proof-maths-menu.el --- Support for maths menu mode package
-;;
-;; Copyright (C) 2007, 2009 LFCS Edinburgh / David Aspinall
+
+;; 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:    David Aspinall <David.Aspinall@ed.ac.uk>
+
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
-;;
+
+;;; Commentary:
 ;;
 ;; With thanks to Dave Love for the original maths menu code,
 ;; provided at http://www.loveshack.ukfsn.org/emacs/
-;;
-;; $Id$
-;;
-;;; Commentary:
 ;; 
 ;; Note: maths menu is bundled with Proof General in lib/, and PG will select
 ;; it's own version before any other version on the Emacs load path.
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 35c6eb3b..f893a9f6 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -1,15 +1,24 @@
 ;;; proof-menu.el --- Menus, keymaps, misc commands for Proof General
-;;
-;; Copyright (C) 2000,2001,2009,2010,2011 LFCS Edinburgh.
+
+;; 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
+
 ;; Authors:   David Aspinall
+
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
+
+;;; Commentary:
 ;;
 
+;;; Code:
 (require 'cl)				; mapcan
 
-;;; Code:
 (eval-when-compile
   (defvar proof-assistant-menu)	  ; defined by macro in proof-menu-define-specific
   (defvar proof-mode-map))
diff --git a/generic/proof-script.el b/generic/proof-script.el
index eb8fac7a..0baf3d5f 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1,12 +1,19 @@
 ;;; proof-script.el --- Major mode for proof assistant script files.
-;;
-;; Copyright (C) 1994-2010 LFCS Edinburgh.
+
+;; 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
+
 ;; Authors:   David Aspinall, Yves Bertot, Healfdene Goguen,
 ;;            Thomas Kleymann and Dilip Sequeira
+
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
+
 ;;; Commentary:
 ;;
 ;; This implements the main mode for script management, including
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 6f3180fe..00d8b1d7 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1,12 +1,19 @@
 ;;; proof-shell.el --- Proof General shell mode.
-;;
-;; Copyright (C) 1994-2011 LFCS Edinburgh.
+
+;; 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
+
 ;; Authors:   David Aspinall, Yves Bertot, Healfdene Goguen,
 ;;            Thomas Kleymann and Dilip Sequeira
+
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
+
 ;;; Commentary:
 ;;
 ;; Mode for buffer which interacts with proof assistant.
diff --git a/generic/proof-site.el b/generic/proof-site.el
index df17229d..c7d721cd 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -1,11 +1,18 @@
-;; proof-site.el -- Loading stubs for Proof General.
-;;
-;; Copyright (C) 1998-2003 LFCS Edinburgh.
+;;; proof-site.el --- Loading stubs 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
+
 ;; Author:      David Aspinall <David.Aspinall@ed.ac.uk>
+
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
+
 ;;; Commentary:
 ;; 
 ;; Loading stubs and configuration for site and choice of provers.
diff --git a/generic/proof-splash.el b/generic/proof-splash.el
index 7e7b8d54..daa09eff 100644
--- a/generic/proof-splash.el
+++ b/generic/proof-splash.el
@@ -1,12 +1,18 @@
-;; proof-splash.el -- Splash welcome screen for Proof General
-;;
-;; Copyright (C) 1998-2005, 2009, 2010 LFCS Edinburgh.
+;;; proof-splash.el --- Splash welcome screen 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
+
 ;; Author:    David Aspinall
+
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
-;;
+
 ;;; Commentary:
 ;; 
 ;; Provide splash screen for Proof General.
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index 84b5940d..cba709d9 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -1,23 +1,27 @@
-;; proof-syntax.el --- Functions for dealing with syntax
-;;
-;; Copyright (C) 1997-2001, 2010 LFCS Edinburgh.
+;;; proof-syntax.el --- Functions for dealing with syntax
+
+;; 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
+
 ;; Authors:   David Aspinall, Healfdene Goguen,
 ;;	      Thomas Kleymann, Dilip Sequiera
-;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
-
-(require 'font-lock)
-(require 'proof-config)			; proof-case-fold-search
-(require 'proof-compat)			; proof-buffer-syntactic-context
-(require 'pg-pamacs)			; proof-ass-sym
 
+;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 
 ;;; Commentary:
 ;; 
 
 ;;; Code:
+(require 'font-lock)
+(require 'proof-config)			; proof-case-fold-search
+(require 'proof-compat)			; proof-buffer-syntactic-context
+(require 'pg-pamacs)			; proof-ass-sym
 
 (defsubst proof-ids-to-regexp (l)
   "Maps a non-empty list of tokens L to a regexp matching any element.
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index af9e8694..88552476 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -1,11 +1,18 @@
 ;;; proof-toolbar.el --- Toolbar for Proof General
-;;
-;; Copyright (C) 1998-2009  David Aspinall / LFCS.
+
+;; 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:    David Aspinall <David.Aspinall@ed.ac.uk>
+
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
+
 ;;; Commentary:
 ;;
 ;; It's a little bit tricky to add prover-specific items:
diff --git a/generic/proof-tree.el b/generic/proof-tree.el
index 438c035e..996934b6 100644
--- a/generic/proof-tree.el
+++ b/generic/proof-tree.el
@@ -1,11 +1,18 @@
 ;;; tree-tree.el --- Proof General prooftree communication.
-;;
-;; Copyright (C) 2012 Hendrik Tews
+
+;; 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
+
 ;; Authors:   Hendrik Tews
+
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
+
 ;;; Commentary:
 ;;
 ;; Generic code for the communication with prooftree. Prooftree
diff --git a/generic/proof-unicode-tokens.el b/generic/proof-unicode-tokens.el
index 0352f012..2deca0e6 100644
--- a/generic/proof-unicode-tokens.el
+++ b/generic/proof-unicode-tokens.el
@@ -1,12 +1,18 @@
 ;;; proof-unicode-tokens.el --- Support Unicode tokens package
-;;
-;; Copyright (C) 2008, 2009 David Aspinall / LFCS Edinburgh
+
+;; 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:    David Aspinall <David.Aspinall@ed.ac.uk>
+
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
-;;
+
 ;;; Commentary:
 ;;
 ;; Support for Unicode Tokens package: per-prover global enabling, copying
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index eb9942a7..b1d8e2e4 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -1,11 +1,18 @@
 ;;; proof-useropts.el --- Global user options for Proof General
-;;
-;; Copyright (C) 2009, 2010, 2011 LFCS Edinburgh.
+
+;; 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:      David Aspinall <David.Aspinall@ed.ac.uk> and others
+
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
+
 ;;; Commentary:
 ;;
 ;; User options for Proof General.
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index dff19e76..575a76ee 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -1,11 +1,18 @@
-;; proof-utils.el --- Proof General utility functions and macros
-;;
-;; Copyright (C) 1998-2002, 2009, 2011 LFCS Edinburgh.
+;;; proof-utils.el --- Proof General utility functions and macros
+
+;; 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:      David Aspinall <David.Aspinall@ed.ac.uk> and others
+
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
+
 ;;; Commentary:
 ;;
 ;; Loading note: this file is required immediately from proof.el, so
diff --git a/generic/proof.el b/generic/proof.el
index 4e7ddbea..5fa9de33 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -1,14 +1,21 @@
 ;;; proof.el --- Proof General theorem prover interface.
-;;
-;; Copyright (C) 1998-2009 LFCS Edinburgh.
+
+;; 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
+
 ;; Authors:   David Aspinall, Yves Bertot, Healfdene Goguen,
 ;;            Thomas Kleymann and Dilip Sequeira
+
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
-;;
+
 ;; Keywords: languages
-;;
-;; $Id$
-;;
+
 ;;; Commentary:
 ;;
 ;; This file loads Proof General.  It is required by the
diff --git a/hol-light/hol-light-autotest.el b/hol-light/hol-light-autotest.el
index 5c1cb011..d68b898f 100644
--- a/hol-light/hol-light-autotest.el
+++ b/hol-light/hol-light-autotest.el
@@ -1,9 +1,20 @@
-;; hol-light-autotest.el: tests of HOL Light Proof General.
+;;; hol-light-autotest.el --- tests of HOL Light 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:
 ;;
 ;; You can run these by issuing "make test.hol-light" in PG home dir.
 ;;
-;; $Id$
-;;
+
+;;; Code:
 
 (eval-when-compile
   (require 'cl))
diff --git a/hol-light/hol-light-unicode-tokens.el b/hol-light/hol-light-unicode-tokens.el
index df32e4bd..7e24e4b1 100644
--- a/hol-light/hol-light-unicode-tokens.el
+++ b/hol-light/hol-light-unicode-tokens.el
@@ -1,8 +1,17 @@
-;;; -*- coding: utf-8; -*-
-;; coq-unicode-tokens.el --- (No) Tokens for Unicode Tokens package
-;;
-;; Copyright(C) 2012 David Aspinall / University of Edinburgh
+;;; coq-unicode-tokens.el --- (No) Tokens for Unicode Tokens package -*- coding: utf-8; -*-
+
+;; 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:    David Aspinall <David.Aspinall@ed.ac.uk>
+
+;;; Commentary:
 ;;
 ;; This file is loaded by `proof-unicode-tokens.el'.
 ;;
@@ -18,6 +27,8 @@
 ;;  - fix unicode tokens sorting so longs tokens handled first (broken?)
 ;;      <=> not <= >
 
+;;; Code:
+
 (require 'proof-unicode-tokens)
 
 (defconst hol-light-token-format "%s")	; plain tokens
diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el
index 467453ed..2b4f3989 100644
--- a/hol-light/hol-light.el
+++ b/hol-light/hol-light.el
@@ -1,15 +1,24 @@
-;; hol-light.el   Basic Proof General instance for HOL Light
-;;
-;; Copyright (C) 2010-12 LFCS Edinburgh, David Aspinall.
-;;
+;;; hol-light.el --- Basic Proof General instance for HOL Light
+
+;; 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: David Aspinall <David.Aspinall@ed.ac.uk>
 ;;         Mark Adams <mark@proof-technologies.com>
-;;
-;; $Id$
+
+;;; Commentary:
 ;;
 ;; See the README file in this directory for information.
 ;;
 
+;;; Code:
+
 (require 'proof-easy-config)            ; easy configure mechanism
 (require 'proof-syntax)			; functions for making regexps
 
diff --git a/hol98/hol98.el b/hol98/hol98.el
index a96da637..6f89707b 100644
--- a/hol98/hol98.el
+++ b/hol98/hol98.el
@@ -1,15 +1,22 @@
-;; hol98.el   Basic Proof General instance for HOL 98
-;;
-;; Copyright (C) 2000 LFCS Edinburgh.
-;;
+;;; hol98.el --- Basic Proof General instance for HOL 98
+
+;; 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: David Aspinall <David.Aspinall@ed.ac.uk>
-;;
-;; $Id$
-;;
+
+;;; Commentary:
 ;; Needs improvement!
 ;;
 ;; See the README file in this directory for information.
 
+;;; Code:
 
 (require 'proof-easy-config)            ; easy configure mechanism
 (require 'proof-syntax)			; functions for making regexps
diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el
index 44a17ade..1cca4cf2 100644
--- a/lego/lego-syntax.el
+++ b/lego/lego-syntax.el
@@ -1,12 +1,23 @@
-;; lego-syntax.el Syntax of LEGO
-;; Copyright (C) 1994 - 1998 LFCS Edinburgh.
+;;; lego-syntax.el --- Syntax of 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 and Dilip Sequeira
-;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Maintainer: Paul Callaghan <P.C.Callaghan@durham.ac.uk>
 
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
+
+;;; Commentary:
 ;;
-;; $Id$
-;;
+
+;;; Code:
 
 (require 'proof-syntax)
 
diff --git a/lego/lego.el b/lego/lego.el
index d1bd7532..29564c87 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -1,12 +1,23 @@
-;; lego.el Major mode for LEGO proof assistants
-;; Copyright (C) 1994 - 1998 LFCS Edinburgh.
+;;; lego.el --- Major mode for LEGO proof assistants
+
+;; 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 and Dilip Sequeira
-;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Maintainer: Paul Callaghan <P.C.Callaghan@durham.ac.uk>
 
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
+
+;;; Commentary:
 ;;
-;; $Id$
-;;
+
+;;; Code:
 
 (require 'proof)
 (require 'lego-syntax)
diff --git a/lib/bufhist.el b/lib/bufhist.el
index 3d6a123d..4c24ca42 100644
--- a/lib/bufhist.el
+++ b/lib/bufhist.el
@@ -1,16 +1,24 @@
 ;; bufhist.el --- keep read-only history of buffer contents for browsing
 
-;; Copyright   (C) 2006, 2009 David Aspinall / University of Edinburgh
+;; 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:     David Aspinall <David.Aspinall@ed.ac.uk>
-;; License:    GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Keywords:   tools
-;;
-;; $Id$
-;;
+
+;; License:    GPL (GNU GENERAL PUBLIC LICENSE)
+
 ;; This file is distributed under the terms of the GNU General Public
 ;; License, Version 2.  Find a copy of the GPL with your version of
 ;; GNU Emacs or Texinfo.
+
+;;; Commentary:
 ;;
 ;; This library implements a minor mode for which keeps a ring history of
 ;; buffer contents.  Intended to be used for small buffers which are
@@ -29,6 +37,8 @@
 ;;         - buttons are put at top of buffer but inserts happen before them
 ;;
 
+;;; Code:
+
 (require 'ring)
 
 (declare-function bufhist-ordinary-erase-buffer "bufhist")
diff --git a/lib/holes.el b/lib/holes.el
index 38a90cfb..2b154723 100644
--- a/lib/holes.el
+++ b/lib/holes.el
@@ -1,9 +1,14 @@
 ;;; holes.el --- a little piece of elisp to define holes in your buffer
-;;
-;; Copyright (C) 2001 Pierre Courtieu
-;;
-;; $Id$
-;;
+
+;; 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
+
 ;; This file uses spans, an interface for extent (XEmacs) and overlays
 ;; (emacs), by Healfdene Goguen for the proofgeneral mode.
 ;;
@@ -11,7 +16,7 @@
 ;; cleaner.
 ;;
 ;; Further cleanups by David Aspinall.
-;;
+
 ;; 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.
@@ -22,19 +27,17 @@
 ;;
 ;; See the GNU General Public License version 2 for more details
 ;; (enclosed in the file GPL).
-;;
-;; See documentation in variable holes-short-doc.
-;;
 
 ;;; Commentary:
 ;;
+;; See documentation in variable holes-short-doc.
+;;
 ;; See documentation of `holes-mode'.
 
+;;; Code:
 (require 'span)
 (require 'cl)
 
-;;; Code:
-
 ;;;
 ;;; initialization
 ;;;
diff --git a/lib/local-vars-list.el b/lib/local-vars-list.el
index 3fa0103d..bcea270f 100644
--- a/lib/local-vars-list.el
+++ b/lib/local-vars-list.el
@@ -1,10 +1,16 @@
 ;;; local-vars.el --- local variables list utilities
-;;
-;; Copyright (C) 2006 Pierre Courtieu
+
+;; 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
+
 ;; Authors: Pierre Courtieu
 ;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
-;;
-;; $Id$
 
 ;; This software is free software; you can redistribute it and/or
 ;; modify it under the terms of the GNU General Public
@@ -18,14 +24,12 @@
 ;; (enclosed in the file GPL).
 
 ;;; Commentary:
+;;
 ;; See documentation in variable local-var-list-doc
-
-;;; TODO: Rely on hack-file-local-variables instead
-
-;;; History:
 ;;
+;; TODO: Rely on hack-file-local-variables instead
 
-;;; Help:
+;;; Code:
 
 (defconst local-vars-list-doc nil
 "From Emacs Info:
diff --git a/lib/maths-menu.el b/lib/maths-menu.el
index b9ddf927..a6b64201 100644
--- a/lib/maths-menu.el
+++ b/lib/maths-menu.el
@@ -1,16 +1,20 @@
 ;;; maths-menu.el --- insert maths characters from a menu  -*-coding: iso-2022-7bit;-*-
 
-;; Copyright (C) 2003, 2012  Free Software Foundation, Inc.
+;; This file is part of Proof General.
+
+;; Portions ,A)(B Copyright 1994-2012  David Aspinall and University of Edinburgh
+;; Portions ,A)(B Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
+;; Portions ,A)(B Copyright 2001-2017  Pierre Courtieu
+;; Portions ,A)(B Copyright 2010, 2016  Erik Martin-Dorel
+;; Portions ,A)(B Copyright 2011-2013, 2016-2017  Hendrik Tews
+;; Portions ,A)(B Copyright 2015-2017  Cl,Ai(Bment Pit-Claudel
 
 ;; Author: Dave Love <fx@gnu.org>
 ;; Keywords: convenience
-
 ;; Version for Proof General modified by David Aspinall, 2007-8.
 ;; - Hooks added to insert tokenised versions of unicode characters.
 ;; - Added more characters to the menus.
 ;; - Define insertion functions following menu names (useful for keybindings)
-;; $Id$
-
 
 ;; This file is free software; you can redistribute it and/or modify
 ;; it under the terms of the GNU General Public License as published by
@@ -49,8 +53,6 @@
 ;; the minibuffer via the menu, though presumably it could be added to
 ;; the minibuffer menu.
 
-
-
 ;;; Code:
 
 (defvar maths-menu-filter-predicate (lambda (char) t)
diff --git a/lib/pg-dev.el b/lib/pg-dev.el
index 758b3d51..79afca23 100644
--- a/lib/pg-dev.el
+++ b/lib/pg-dev.el
@@ -1,11 +1,18 @@
 ;;; pg-dev.el --- Developer settings for Proof General
-;;
-;; Copyright (C) 2008-2011 LFCS Edinburgh.
+
+;; 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:      David Aspinall <David.Aspinall@ed.ac.uk> and others
+
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
- ;;
+
 ;;; Commentary:
 ;;
 ;; Some configuration of Emacs Lisp mode for developing PG, not needed
diff --git a/lib/pg-fontsets.el b/lib/pg-fontsets.el
index c4d76efc..771e76f1 100644
--- a/lib/pg-fontsets.el
+++ b/lib/pg-fontsets.el
@@ -1,11 +1,18 @@
 ;;; pg-fontsets.el --- Define fontsets useful for Proof General
-;;
-;; Copyright (C) 2008 David Aspinall / LFCS Edinburgh
+
+;; 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:    David Aspinall <David.Aspinall@ed.ac.uk>
+
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
+
 ;;; Commentary:
 ;;
 ;; Define some fontsets to try to select fonts that display many symbols.
diff --git a/lib/proof-compat.el b/lib/proof-compat.el
index 4eb942cb..4c1fa5b2 100644
--- a/lib/proof-compat.el
+++ b/lib/proof-compat.el
@@ -1,10 +1,19 @@
-;; proof-compat.el   Operating system and Emacs version compatibility
-;;
-;; Copyright (C) 2000-2010 LFCS Edinburgh.
+;;; proof-compat.el --- Operating system and Emacs version compatibility
+
+;; 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:      David Aspinall <David.Aspinall@ed.ac.uk> and others
+
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
+
+;;; Commentary:
 ;;
 ;; This file collects together compatibility hacks for different
 ;; operating systems and Emacs versions.  This is to help keep
@@ -17,6 +26,8 @@
 ;; Since Proof General 4.0, XEmacs is not supported at all.
 ;;
 
+;;; Code:
+
 (require 'easymenu)
 (require 'cl)
 
diff --git a/lib/scomint.el b/lib/scomint.el
index af8df997..3644add2 100644
--- a/lib/scomint.el
+++ b/lib/scomint.el
@@ -1,10 +1,17 @@
 ;;; scomint.el --- Simplified comint for less interactive shells
-;;
-;; Copyright (C) 2009 LFCS Edinburgh.
+
+;; 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:    David Aspinall
+
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
 
 ;;; Commentary:
 ;;
@@ -16,6 +23,8 @@
 ;; hard to disentangle.
 ;;
 
+;;; Code:
+
 (defvar scomint-buffer-maximum-size 800000
   "The maximum size in characters for SComint buffers.
 SComint buffers are truncated from the top to be no greater than this number,
diff --git a/lib/span.el b/lib/span.el
index f1379616..2252d605 100644
--- a/lib/span.el
+++ b/lib/span.el
@@ -1,12 +1,19 @@
 ;;; span.el --- Datatype of "spans" for Proof General
-;;
-;; Copyright (C) 1998-2009 LFCS Edinburgh
+
+;; 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:      Healfdene Goguen
 ;; Maintainer:  David Aspinall <David.Aspinall@ed.ac.uk>
+
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
+
 ;;; Commentary:
 ;;
 ;; Spans are our abstraction of extents/overlays.  Nowadays
@@ -16,6 +23,7 @@
 ;;
 
 ;;; Code:
+
 (eval-when-compile (require 'cl))       ;For lexical-let.
 
 (defalias 'span-start 'overlay-start)
diff --git a/lib/texi-docstring-magic.el b/lib/texi-docstring-magic.el
index 6e8c8e49..93896209 100644
--- a/lib/texi-docstring-magic.el
+++ b/lib/texi-docstring-magic.el
@@ -1,16 +1,24 @@
-;; texi-docstring-magic.el --- munge internal docstrings into texi
-;;
-;; Keywords: lisp, docs, tex
+;;; texi-docstring-magic.el --- munge internal docstrings into texi
+
+;; 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:     David Aspinall <David.Aspinall@ed.ac.uk>
-;; Copyright   (C) 1998 David Aspinall
+;; Keywords: lisp, docs, tex
+
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
+
 ;; This file is distributed under the terms of the GNU General Public
 ;; License, Version 2.  Find a copy of the GPL with your version of
 ;; GNU Emacs or Texinfo.
-;;
+
+;;; Commentary:
 ;;
 ;; This package generates Texinfo source fragments from Emacs
 ;; docstrings.  This avoids documenting functions and variables in
@@ -82,6 +90,8 @@
 ;;
 ;;
 
+;;; Code:
+
 (eval-when-compile
   (require 'cl))
 
diff --git a/lib/unicode-chars.el b/lib/unicode-chars.el
index 1e5dedbf..880371ce 100644
--- a/lib/unicode-chars.el
+++ b/lib/unicode-chars.el
@@ -1,7 +1,17 @@
-;; unicode-chars.el --- table of Unicode characters
-;;
+;;; unicode-chars.el --- table of Unicode characters
+
+;; 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:    David Aspinall
-;; $Id$
+
+;;; Commentary:
 ;;
 ;; Adapted from Norman Walsh's unichars.el (iso8879 names removed)
 ;;
@@ -9,6 +19,8 @@
 ;; http://www.unicode.org/unicode/standard/standard.html
 ;; http://www.unicode.org/Public/UNIDATA
 
+;;; Code:
+
 (defvar unicode-chars-alist
   '(;Unicode name  Codept
     ("NULL" . #x000000)
diff --git a/lib/unicode-tokens.el b/lib/unicode-tokens.el
index d05bfc1e..e98ca0a2 100644
--- a/lib/unicode-tokens.el
+++ b/lib/unicode-tokens.el
@@ -1,11 +1,18 @@
 ;;; unicode-tokens.el --- Support for control and symbol tokens
-;;
-;; Copyright(C) 2008-2010 David Aspinall / LFCS Edinburgh
+
+;; 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:    David Aspinall <David.Aspinall@ed.ac.uk>
+
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
+
 ;; This 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 2, or (at your option)
@@ -37,9 +44,7 @@
 ;; -- simplify/optimise property handling
 ;; -- support multiple modes with mode-local configs at once
 
-;;
 ;;; Code:
-;;
 
 (require 'cl)
 (require 'quail)
diff --git a/pg-init.el b/pg-init.el
index 8fca25de..bdc6e4ea 100644
--- a/pg-init.el
+++ b/pg-init.el
@@ -1,6 +1,13 @@
 ;;; pg-init.el --- Init file used for compatibility with package.el and ELPA  -*- lexical-binding: t; -*-
 
-;; Copyright (C) 2017  Clément Pit-Claudel
+;; 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: Clément Pit-Claudel <clement.pitclaudel@live.com>
 
@@ -18,7 +25,7 @@
 ;; along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 ;;; Commentary:
-
+;;
 ;; 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.
diff --git a/pghaskell/pghaskell.el b/pghaskell/pghaskell.el
index f2aec426..7784cf0f 100644
--- a/pghaskell/pghaskell.el
+++ b/pghaskell/pghaskell.el
@@ -1,6 +1,17 @@
-;; pghaskell.el - Proof General for Haskell scripts.
-;;
-;; David Aspinall.  $Id$
+;;; pghaskell.el --- Proof General for Haskell scripts.
+
+;; 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: David Aspinall.
+
+;;; Commentary:
 ;;
 ;; This instance of PG is handy just for using script management to
 ;; cut-and-paste into a buffer running Haskell (ghci)
@@ -18,6 +29,7 @@
 ;; in proof-site.el).
 ;;
 
+;;; Code:
 
 (require 'proof-easy-config)
 (require 'proof-syntax)
diff --git a/pgocaml/pgocaml.el b/pgocaml/pgocaml.el
index 4b11c7df..dcf179d0 100644
--- a/pgocaml/pgocaml.el
+++ b/pgocaml/pgocaml.el
@@ -1,6 +1,17 @@
-;; pgocaml.el - Proof General for OCaml scripts.
-;;
-;; David Aspinall.  $Id$
+;;; pgocaml.el --- Proof General for OCaml scripts.
+
+;; 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: David Aspinall
+
+;;; Commentary:
 ;;
 ;; This instance of PG is handy just for using script management to
 ;; cut-and-paste into a buffer running OCaml
@@ -18,6 +29,7 @@
 ;; in proof-site.el).
 ;;
 
+;;; Code:
 
 (require 'proof-easy-config)
 (require 'proof-syntax)
diff --git a/pgshell/pgshell.el b/pgshell/pgshell.el
index aa34e985..39c780dc 100644
--- a/pgshell/pgshell.el
+++ b/pgshell/pgshell.el
@@ -1,6 +1,17 @@
-;; pgshell.el - Proof General for shell scripts.
-;;
-;; David Aspinall.  $Id$
+;;; pgshell.el --- Proof General for shell scripts.
+
+;; 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: David Aspinall.
+
+;;; Commentary:
 ;;
 ;; This instance of PG is handy just for using script management to
 ;; cut-and-paste into a buffer running an ordinary shell of some kind.
@@ -13,6 +24,7 @@
 ;;
 ;; Feedback welcome.
 
+;;; Code:
 
 (require 'proof-easy-config)
 (require 'proof-syntax)