emacs-elpa-diffs
[Top][All Lists]
Advanced

[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



reply via email to

[Prev in Thread] Current Thread [Next in Thread]