From a23ca01c680d2cf63de8b008ec44b8cbacf5f89e Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Thu, 7 Sep 2006 17:25:33 +0000
Subject: Added Goal as a goal starter in syntax db.

---
 coq/coq-syntax.el | 1 +
 1 file changed, 1 insertion(+)

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 20cad0f7..87eac7c0 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -349,6 +349,7 @@ so for the following reasons:
     ("Declare Module <:" "dmi2" "Declare Module # <: #.\n#\nEnd #." t)
     ("Definition" "def" "Definition #:# := #." t "Definition");; careful
     ("Fact" "fct" "Fact # : #." t "Fact")
+    ("Goal" nil "Goal #." t "Goal")
     ("Lemma" "l" "Lemma # : #.\nProof.\n#\nQed." t "Lemma")
     ("Module! (interactive)" nil "Module # : #.\n#\nEnd #." nil nil coq-insert-section-or-module)
     ("Module :" "moi" "Module # : #.\n#\nEnd #." t "Module") ; careful
-- 
cgit v1.2.3