Update copyright messages and improve the header of elisp files.

14 files changed, 199 insertions, 60 deletions

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)