diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-10-06 17:33:52 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-10-06 17:33:52 +0000 |
| commit | 51f8779b1a54a29670be2ca8dd3ac9e9c1f3f9b6 (patch) | |
| tree | 9b2e2b12a46a0ae47e771791f53a1239455241aa | |
| parent | 29c93767fd12ff1fd1172ce1aa7b2bc378f77aa6 (diff) | |
Fix for Unnamed_thm: Coq really uses this identifier.
| -rw-r--r-- | coq/coq.el | 14 |
1 files changed, 8 insertions, 6 deletions
@@ -190,12 +190,13 @@ ((eq (span-property span 'type) 'comment)) ((eq (span-property span 'type) 'goalsave) - ;; FIXME da 5.10.99: I added in this test for an unnamed - ;; theorem. Probably it is harmless (it's a new case for LEGO - ;; and Isabelle). - (unless (eq (span-property span 'name) proof-unnamed-theorem-name) - (setq ans (concat lego-forget-id-command - (span-property span 'name) proof-terminal-string)))) + ;; Note da 6.10.99: in Lego and Isabelle, it's trivial to + ;; forget an unnamed theorem. Coq really does use the + ;; identifier "Unnamed_thm", though! So we don't need + ;; this test: + ;; (unless (eq (span-property span 'name) proof-unnamed-theorem-name) + (setq ans (concat coq-forget-id-command + (span-property span 'name) proof-terminal-string))) ((proof-string-match (concat "\\`\\(" coq-keywords-decl-defn-regexp "\\)\\s-*\\(" proof-id "\\)\\s-*[\\[,:]") str) @@ -410,6 +411,7 @@ (setq proof-terminal-char ?\.) (setq proof-comment-start "(*") (setq proof-comment-end "*)") + (setq proof-unnamed-theorem-name "Unnamed_thm") ; Coq's default name (setq proof-assistant-home-page coq-www-home-page) |