diff options
| author | David Aspinall | 1998-11-03 14:40:52 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-11-03 14:40:52 +0000 |
| commit | 6d570f591af3d4aa5ded571cea0b70bd83e362fa (patch) | |
| tree | 13eb3b9b4f6e3b62cb18dd597e5fe5efcd249702 /generic | |
| parent | aaaeaeb988028e4445a91ac60c2700ddbdf577b2 (diff) | |
Note added.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-script.el | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index cefcbd39..93e54789 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -553,7 +553,8 @@ the ACS is marked in the current buffer. If CMD does not match any, (setq nam (match-string 2 (span-property gspan 'cmd))) ;; This only works for Coq, but LEGO raises an error if ;; there's no name. - ;; FIXME: a nonsense for Isabelle. + ;; FIXME da: maybe this should be prover specific: is + ;; "Unnamed_thm" actually a Coq identifier? (setq nam "Unnamed_thm"))) (set-span-end gspan end) |