added support for etags at generic proof level

3 files changed, 11 insertions, 8 deletions

diff --git a/coq.el b/coq.el
index 78655eb6..0cfccd3d 100644
--- a/coq.el
+++ b/coq.el
@@ -3,6 +3,9 @@
 ;; Author: Healfdene Goguen and Thomas Kleymann
 
 ;; $Log$
+;; 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
@@ -561,10 +564,6 @@
 
   (proof-config-done)
 
-;  (define-key (current-local-map) [(meta tab)]
-;    (if (fboundp 'complete-tag)
-;	'complete-tag		; Emacs 19.31 (superior etags)
-;      'tag-complete-symbol))	;XEmacs 19.13 (inferior etags)
   (define-key (current-local-map) [(control c) (control p)] 'coq-prf)
   (define-key (current-local-map) [(control c) c] 'coq-ctxt)
   (define-key (current-local-map) [(control c) h] 'coq-help)
diff --git a/lego.el b/lego.el
index 515dba5e..75f1f9ba 100644
--- a/lego.el
+++ b/lego.el
@@ -5,6 +5,9 @@
 
 
 ;; $Log$
+;; Revision 1.37  1998/03/25 17:30:41  tms
+;; added support for etags at generic proof level
+;;
 ;; Revision 1.36  1998/02/10 14:12:56  tms
 ;; added Dnf to lego-undoable-commands-regexp
 ;;
@@ -599,10 +602,6 @@
 
   (proof-config-done)
 
-  (define-key (current-local-map) [(meta tab)]
-    (if (fboundp 'complete-tag)
-	'complete-tag		; Emacs 19.31 (superior etags)
-      'tag-complete-symbol))	;XEmacs 19.13 (inferior etags)
   (define-key (current-local-map) [(control c) (control p)] 'lego-prf)
   (define-key (current-local-map) [(control c) c] 'lego-ctxt)
   (define-key (current-local-map) [(control c) h] 'lego-help)
diff --git a/proof.el b/proof.el
index 30893c11..0fcde1a1 100644
--- a/proof.el
+++ b/proof.el
@@ -9,6 +9,9 @@
 
 
 ;; $Log$
+;; Revision 1.35  1998/03/25 17:30:28  tms
+;; added support for etags at generic proof level
+;;
 ;; Revision 1.34  1998/03/24 17:26:15  tms
 ;; *** empty log message ***
 ;;
@@ -1478,6 +1481,8 @@ current command."
 
 ;; keymap
 
+  (define-key proof-mode-map [(meta tab)] 'tag-complete-symbol)
+
   (define-key proof-mode-map
     (vconcat [(control c)] (vector proof-terminal-char))
     'proof-active-terminator-minor-mode)