diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-10-06 11:18:56 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-10-06 11:18:56 +0000 |
| commit | d4316a2d63c9c2b12cdce73e62cd435d7ff01002 (patch) | |
| tree | c5eff6a0c98f2d73725cba83d4f0ceea1b9fa6ec /coq | |
| parent | a7928b121ae5c356eac5e2f48f32faca404a7ce3 (diff) | |
More improvements/fixes for closing unfinished proofs.
Added proof-unnamed-theorem-name.
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq.el | 8 |
1 files changed, 6 insertions, 2 deletions
@@ -190,8 +190,12 @@ ((eq (span-property span 'type) 'comment)) ((eq (span-property span 'type) 'goalsave) - (setq ans (concat coq-forget-id-command - (span-property span 'name) proof-terminal-string))) + ;; 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)))) ((proof-string-match (concat "\\`\\(" coq-keywords-decl-defn-regexp "\\)\\s-*\\(" proof-id "\\)\\s-*[\\[,:]") str) |