aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-seq-compile.el
diff options
context:
space:
mode:
Diffstat (limited to 'coq/coq-seq-compile.el')
-rw-r--r--coq/coq-seq-compile.el21
1 files changed, 15 insertions, 6 deletions
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))