From 4e0c2a00cfbb7ea5c5ab68573bfb0edb78e8bd6f Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel <erik@martin-dorel.org>
Date: Sat, 12 Aug 2017 13:48:08 +0200
Subject: Update copyright messages and improve the header of elisp files.

---
 hol-light/hol-light-autotest.el       | 17 ++++++++++++++---
 hol-light/hol-light-unicode-tokens.el | 19 +++++++++++++++----
 hol-light/hol-light.el                | 21 +++++++++++++++------
 3 files changed, 44 insertions(+), 13 deletions(-)

(limited to 'hol-light')

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
 
-- 
cgit v1.2.3