From 5336774f943006195f5b378ed75ca99d9941bf90 Mon Sep 17 00:00:00 2001
From: Healfdene Goguen
Date: Wed, 12 Nov 1997 15:56:15 +0000
Subject: Changed pbp-change-goal so that it only "Show"s the goal pointed at.

---
 coq.el | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/coq.el b/coq.el
index bb53cace..202dfdff 100644
--- a/coq.el
+++ b/coq.el
@@ -3,6 +3,9 @@
 ;; Author: Healfdene Goguen and Thomas Kleymann
 
 ;; $Log$
+;; 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
@@ -521,7 +524,7 @@
 )
 
 (defun coq-pbp-mode-config ()
-  (setq pbp-change-goal "Focus %s.")
+  (setq pbp-change-goal "Show %s.")
   (setq pbp-error-regexp coq-error-regexp))
 
 (provide 'coq)
-- 
cgit v1.2.3