[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/proof-general 78a555a12d 2/2: coq/coq.el: add a tiny bit o
From: |
ELPA Syncer |
Subject: |
[nongnu] elpa/proof-general 78a555a12d 2/2: coq/coq.el: add a tiny bit of documentation (#693) |
Date: |
Sun, 26 Mar 2023 20:02:53 -0400 (EDT) |
branch: elpa/proof-general
commit 78a555a12dd40348fb098331a20aa6fd663c152d
Author: hendriktews <hendrik@askra.de>
Commit: GitHub <noreply@github.com>
coq/coq.el: add a tiny bit of documentation (#693)
---
coq/coq.el | 2 ++
1 file changed, 2 insertions(+)
diff --git a/coq/coq.el b/coq/coq.el
index 5a85bf7b9d..5de2374fa9 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -722,6 +722,7 @@ If locked span already has a state number, then do nothing.
Also updates
"Last goal that Emacs looked at.")
(defun coq-goal-hyp ()
+ "Instanciation for `pg-topterm-goalhyplit-fn', see there."
(cond
((looking-at "============================\n")
(goto-char (match-end 0))
@@ -735,6 +736,7 @@ If locked span already has a state number, then do nothing.
Also updates
(t nil)))
(defun coq-state-preserving-p (cmd)
+ "Instanciation for `proof-state-preserving-p', see there."
;; (or
(proof-string-match coq-non-retractable-instruct-regexp cmd))
;; (and