diff options
| author | Pierre Courtieu | 2006-08-25 18:19:17 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2006-08-25 18:19:17 +0000 |
| commit | 1a3b2c68197b7b2bd5144ec7bfa86108fa1e9e1c (patch) | |
| tree | 95045288ce0db7a80a3633066f6c5deae7eed3ab | |
| parent | ac2ed5ec6a3fee36abd1ca0aca2f049c1ce0fb01 (diff) | |
Small fixes on syntax tables.
| -rw-r--r-- | coq/coq-syntax.el | 7 | ||||
| -rw-r--r-- | coq/coq.el | 2 |
2 files changed, 6 insertions, 3 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 0c96a79b..aac4600c 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -228,6 +228,9 @@ so for the following reasons: ("set in" "seti" "set ( # := #) in #" t) ("set" "set" "set ( # := #)" t "set") ("setoid_replace with" "strep" "setoid_replace # with #" t "setoid_replace") + ("setoid replace with" "strep" "setoid replace # with #" t "setoid\\s-+replace") + ("setoid_rewrite" "strew" "setoid_rewrite #" t "setoid_rewrite") + ("setoid rewrite" "strew" "setoid rewrite #" t "setoid\\s-+rewrite") ("simpl" "s" "simpl" t "simpl") ("simpl" "sa" "simpl # at #" t) ("simple destruct" "sdes" "simple destruct" t "simple\\s-+destruct") @@ -345,7 +348,7 @@ so for the following reasons: ("Declare Module :" "dmi" "Declare Module # : #.\n#\nEnd #." t) ("Declare Module <:" "dmi2" "Declare Module # <: #.\n#\nEnd #." t) ("Definition" "def" "Definition #:# := #." t "Definition");; careful - ("Fact" "l" "Fact # : #." t "Fact") + ("Fact" "fct" "Fact # : #." t "Fact") ("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 @@ -353,7 +356,7 @@ so for the following reasons: ("Module Type" "mti" "Module Type #.\n#\nEnd #." t "Module\\s-+Type") ; careful ("Remark" "l" "Remark # : #.\n#\nQed." t "Remark") ("Section" "sec" "Section #." t "Section") - ("Theorem" "l" "Theorem # : #.\n#\nQed." t "Theorem") + ("Theorem" "t" "Theorem # : #.\n#\nQed." t "Theorem") ) "Coq goal starters keywords information list. See `coq-syntax-db' for syntax. " ) @@ -448,7 +448,7 @@ If locked span already has a state number, thne do nothing. Also updates (defun coq-find-and-forget-v81 (span) "Backtrack to SPAN. Using the \"Backtrack n m p\" coq command." - (let* (str ans (naborts 0) (nundos 0) + (let* (ans (naborts 0) (nundos 0) (proofdepth (coq-get-span-proofnum span)) (proofstack (coq-get-span-proofstack span)) (span-staten (coq-get-span-statenum span)) |