Updated the doc for new pg/coq. Made modifications advised by Stefan

Monnier on holes.el.

2 files changed, 8 insertions, 3 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index cef21e06..d2e31539 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -1,6 +1,10 @@
 ;; default abbrev table
 ; This is for coq V8, you should test coq version before loading
 
+(defun holes-show-doc () 
+  (interactive)
+  (describe-variable 'holes-doc))
+
 ;#s are replaced by holes by holes-abbrev-complete
 (if (boundp 'holes-abbrev-complete)
 	 ()
@@ -312,7 +316,7 @@
      ["Replace active hole by selection"  holes-replace-update-active-hole t]
      ["Jump to active hole"  holes-set-point-next-hole-destroy t]
      ["Forget all holes in buffer"  holes-clear-all-buffer-holes t]
-     ["Tell me about holes?" holes-short-doc t]
+     ["Tell me about holes?" holes-show-doc t]
      ;; look a bit better at the bottom
      "Make hole with mouse: C-M-select"
      "Replace hole with mouse: C-M-Shift select"  ;; da: does this one work??
@@ -339,7 +343,7 @@
 ;; da: Moved this from the main menu to the Help submenu.  
 ;; It also appears under Holes, anyway.
 (defpgdefault help-menu-entries
-  '(["Tell me about holes?" holes-short-doc t]))
+  '(["Tell me about holes?" holes-show-doc t]))
 
 
 (provide 'coq-abbrev)
diff --git a/coq/coq.el b/coq/coq.el
index 6735ca42..d034ff92 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -363,7 +363,8 @@ toplevel \"Coq <\". Returns nil if yes. This assumes that no
        ;; if nabort<>0 then current goal is actually aborted
        ((and (coq-proof-mode-p) (coq-state-changing-tactic-p str) (= naborts 0))
         (incf nundos))
-       ;; default case: command, do nothing (BackTo will deal with this)
+       ;; default case: command or state preserving tactic, do nothing (BackTo will
+       ;; deal with this)
        (t ())
        )
       ;;go to next span