diff options
| author | Christophe Raffalli | 2000-10-27 07:38:19 +0000 |
|---|---|---|
| committer | Christophe Raffalli | 2000-10-27 07:38:19 +0000 |
| commit | 60ce91371d746bf08e3c3b48ce7c1e1304580252 (patch) | |
| tree | aaf839b8153bbdda093ae3723d7ae902f44599db /generic/proof-script.el | |
| parent | 028d8da63899286c4bf9c3aa83ce460d07996861 (diff) | |
*** empty log message ***
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index fe6c07ac..36423c20 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1004,8 +1004,8 @@ the ACS is marked in the current buffer. If CMD does not match any, (let (nam gspan next) ;; Try to set the name of the theorem from the save - (setq cmd (proof-remove-comment cmd)) (and proof-save-with-hole-regexp + (setq cmd (proof-remove-comment cmd)) (proof-string-match proof-save-with-hole-regexp cmd) (setq nam (match-string 2 cmd))) @@ -1025,11 +1025,12 @@ the ACS is marked in the current buffer. If CMD does not match any, "Proof General: script management confused, couldn't find goal span for save.") ;; If the name isn't set, try to set it from the goal. - (let ((cmdstr (proof-remove-comment (span-property gspan 'cmd)))) (unless nam (and proof-goal-with-hole-regexp - (proof-string-match proof-goal-with-hole-regexp cmdstr) - (setq nam (match-string 2 cmdstr))))) + (let ((cmdstr + (proof-remove-comment (span-property gspan 'cmd)))) + (proof-string-match proof-goal-with-hole-regexp cmdstr) + (setq nam (match-string 2 cmdstr))))) ;; As a final desparate attempt, set the name to ;; proof-unnamed-theorem-name (Coq actually uses a default |