minor modifications

2 files changed, 3 insertions, 188 deletions

diff --git a/coq.el b/coq.el
index 4c198485..3a34ab19 100644
--- a/coq.el
+++ b/coq.el
@@ -1,151 +1,8 @@
 ;; coq.el Major mode for Coq proof assistant
-;; Copyright (C) 1994, 1995, 1996, 1997 LFCS Edinburgh. 
+;; Copyright (C) 1994 - 1998 LFCS Edinburgh. 
 ;; Author: Healfdene Goguen and Thomas Kleymann
 
-;; $Log$
-;; Revision 2.2  1998/09/03 11:26:55  da
-;; Dead code.
-;;
-;; Revision 2.1  1998/09/03 11:07:07  da
-;; Removed dead code
-;;
-;; Revision 2.0  1998/08/11 11:39:20  da
-;; Renamed <file>-fontlock to <file>-syntax
-;;
-;; Revision 1.29  1998/06/10 11:42:06  hhg
-;; Added coq-init-syntax-table as function to initialize syntax entries
-;; particular to coq.
-;; Changed proof-ctxt-string to "Print All".
-;; Call coq-init-syntax-table from coq-shell-mode-config.  This was
-;; necessary to get prompts with "'"s in them (coming from goals with
-;; same) recognized.
-;;
-;; Revision 1.28  1998/06/03 18:02:54  hhg
-;; Added '?'s before single characters in define-keys for emacs19, at
-;; Pascal Brisset's suggestion.
-;;
-;; Revision 1.27  1998/06/03 13:57:10  hhg
-;; Added definition of proof-commands-regexp for coq
-;;
-;; Revision 1.26  1998/06/02 15:34:43  hhg
-;; Generalized proof-retract-target, now parameterized by
-;; proof-count-undos and proof-find-and-forget.
-;; Generalized proof-shell-analyse-structure, introduced variable
-;; proof-analyse-using-stack.
-;; Generalized proof menu plus ancillary functions.
-;; Generalized proof-mode-version-string.
-;; Moved various comments into documentation string.
-;;
-;; Revision 1.25  1998/05/23 12:50:40  tms
-;; improved support for Info
-;;   o employed `Info-default-directory-list' rather than
-;;     `Info-directory-list' so that code also works for Emacs 19.34
-;;   o setting of `Info-default-directory-list' now at proof level
-;;
-;; Revision 1.24  1998/05/22 11:31:33  hhg
-;; Correct path for coq-prog-name and coq-tags.
-;;
-;; Revision 1.23  1998/05/15 16:16:55  hhg
-;; Changed variable names [s]ext to span.
-;; Fixed coq-find-and-forget pattern for declarations and definitions
-;; following Pascal Brisset's suggestion.
-;;
-;; Revision 1.22  1998/05/14 11:52:32  hhg
-;; Changes to indentation code:
-;; 	Changed "case" to "Case".
-;; 	Added "CoInductive".
-;;
-;; Revision 1.21  1998/05/12 14:51:27  hhg
-;; Added hook `coq-shell-init-hook', for `proof-shell-insert-hook'.
-;; This initializes undo limit and changes directory to that associated
-;; with buffer.
-;; This is because Coq has a command line option to run with emacs mode.
-;;
-;; Revision 1.20  1998/05/08 17:08:31  hhg
-;; Made separated indentation more elegant.
-;; 	Fixed bug with Inductive.
-;; 	Added CoInductive.
-;;
-;; Revision 1.19  1998/05/08 15:42:42  hhg
-;; Merged indentation code for LEGO and Coq into proof.el.
-;;
-;; Revision 1.18  1998/05/06 16:39:10  hhg
-;; Removed default instantiation of undo limit to 100.
-;;
-;; Revision 1.17  1998/05/06 15:29:11  hhg
-;; Added coq-info-dir so that script-management.info can be hard-coded.
-;;
-;; Revision 1.16  1998/05/05 14:21:48  hhg
-;; Made updates to fix problem with Definition, which couldn't be
-;; used with proof scripts.
-;; Removed some useless declarations.
-;; Removed Abort from menu.
-;; Now Reset's if user undoes to beginning of proof.
-;; Added command to increase undo limit for Coq, and set default to 100.
-;;
-;; Revision 1.15  1998/03/25 17:30:35  tms
-;; added support for etags at generic proof level
-;;
-;; Revision 1.14  1998/01/15 13:30:18  hhg
-;; Added coq-shell-cd
-;; Some new fontlocks
-;;
-;; Revision 1.13  1997/11/26 17:23:51  hhg
-;; Added C-c C-s to run "Search" in Coq.
-;; Moved coq-goal-with-hole-regexp etc to coq-fontlock.
-;; Removed various superfluous definitions for COQPATH etc.
-;;
-;; Revision 1.12  1997/11/24 19:15:08  djs
-;; Added proof-execute-minibuffer-cmd and scripting minor mode.
-;;
-;; Revision 1.11  1997/11/20 13:03:08  hhg
-;; Added coq-global-p for global declarations and definitions.  These now
-;; get lifted in the same way as lemmas.
-;; Changed [meta (control i)] to [meta tab] in key definition.
-;; Changed menu, and made help in menu refer to info mode.
-;;
-;; Revision 1.10  1997/11/17 17:11:15  djs
-;; Added some magic commands: proof-frob-locked-end, proof-try-command,
-;; proof-interrupt-process. Added moving nested lemmas above goal for coq.
-;; Changed the key mapping for assert-until-point to C-c RET.
-;;
-;; Revision 1.9  1997/11/12 15:56:15  hhg
-;; Changed pbp-change-goal so that it only "Show"s the goal pointed at.
-;;
-;; Revision 1.8  1997/11/06 16:55:49  hhg
-;; Assign new variable proof-goal-hyp-fn to coq-goal-hyp, which advances
-;; over coq-goal-regexp to pick up goal for pbp
-;;
-;; Revision 1.7  1997/10/30 15:58:31  hhg
-;; Updates for coq, including:
-;; 	* pbp-goal-command and pbp-hyp-command use proof-terminal-string
-;; 	* updates to keywords
-;; 	* fix for goal regexp
-;;
-;; Revision 1.6  1997/10/24 14:51:09  hhg
-;; Fixed coq-count-undos for comments
-;;
-;; Revision 1.5  1997/10/17 14:51:48  hhg
-;; Fixed coq-shell-prompt-pattern to reflect proof-id
-;; Changed ";" to "." in coq-save-with-hole-regexp
-;; New modifications to syntax table to reflect actual use of symbols in Coq
-;;
-;; Revision 1.4  1997/10/16 13:14:32  djs
-;; Merged Coq changes with main branch.
-;;
-;; Revision 1.2  1997/10/13 17:12:48  tms
-;; *** empty log message ***
-;;
-;; Revision 1.1.2.3  1997/10/10 19:19:58  djs
-;; Added multiple file support, changed the way comments work, fixed a
-;; few minor bugs, and merged in coq support by hhg.
-;;
-;; Revision 1.1.2.2  1997/10/08 08:22:30  hhg
-;; Updated undo, fixed bugs, more modularization
-;;
-;; Revision 1.1.2.1  1997/10/07 13:34:16  hhg
-;; New structure to share as much as possible between LEGO and Coq.
-;;
+;; $Id$
 
 (require 'coq-syntax)
 (require 'outline)
diff --git a/proof-syntax.el b/proof-syntax.el
index 45c9015d..5caa8fe3 100644
--- a/proof-syntax.el
+++ b/proof-syntax.el
@@ -1,50 +1,8 @@
 ;; proof-syntax.el Generic font lock expressions
-;; Copyright (C) 1997 LFCS Edinburgh. 
+;; Copyright (C) 1997-1998 LFCS Edinburgh. 
 ;; Author: Healfdene Goguen, Thomas Kleymann and Dilip Sequiera
 ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
 
-;; $Log$
-;; Revision 2.0  1998/08/11 15:00:04  da
-;; New branch
-;;
-;; Revision 1.2  1998/08/11 11:43:14  da
-;; Renamed <file>-fontlock to <file>-syntax
-;;
-;; Revision 1.8  1998/06/10 11:45:12  hhg
-;; Changed "\\s " to "\\s-" in proof-id as whitespace pattern.
-;;
-;; Revision 1.7  1998/05/29 09:49:53  tms
-;; o outsourced indentation to proof-indent
-;; o support indentation of commands
-;; o replaced test of Emacs version with availability test of specific
-;;   features
-;; o C-c C-c, C-c C-v and M-tab is now available in all buffers
-;;
-;; Revision 1.6  1998/05/06 15:56:14  hhg
-;; Fixed problem introduced by working on emacs19 in
-;; proof-zap-commas-region.
-;;
-;; Revision 1.5  1998/05/05 14:25:45  hhg
-;; Simple white-space changes.
-;;
-;; Revision 1.4  1998/01/16 15:40:28  djs
-;; Commented the code of proof.el and lego.el a bit. Made a minor change
-;; to the way errors are handled, so that any delayed output is inserted
-;; in the buffer before the error message is printed.
-;;
-;; Revision 1.3  1997/11/17 17:11:19  djs
-;; Added some magic commands: proof-frob-locked-end, proof-try-command,
-;; proof-interrupt-process. Added moving nested lemmas above goal for coq.
-;; Changed the key mapping for assert-until-point to C-c RET.
-;;
-;; Revision 1.2  1997/10/13 17:13:50  tms
-;; *** empty log message ***
-;;
-;; Revision 1.1.2.1  1997/10/07 13:34:27  hhg
-;; New structure to share as much as possible between LEGO and Coq.
-;;
-;;
-
 (require 'font-lock)
 
 ;;; FIXME: change this to proof-