From 51f8779b1a54a29670be2ca8dd3ac9e9c1f3f9b6 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 6 Oct 1999 17:33:52 +0000 Subject: Fix for Unnamed_thm: Coq really uses this identifier. --- coq/coq.el | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/coq/coq.el b/coq/coq.el index daa71eb6..d355a4c0 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -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) -- cgit v1.2.3