diff options
| author | Pierre Courtieu | 2006-09-07 17:25:33 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2006-09-07 17:25:33 +0000 |
| commit | a23ca01c680d2cf63de8b008ec44b8cbacf5f89e (patch) | |
| tree | 695aae79697766e83330f5123542bb0194df918c /coq | |
| parent | 6d73195f7b3e976f2df62d13f029f55558cde5fd (diff) | |
Added Goal as a goal starter in syntax db.
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-syntax.el | 1 |
1 files changed, 1 insertions, 0 deletions
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 |