diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2004-03-18 10:21:16 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2004-03-18 10:21:16 +0000 |
| commit | 0ce0b8071577f7edd546b1e12135021bdbfeac10 (patch) | |
| tree | 27c97cd13b17eaaa03a8736edbdee5b4aaa5f63d /coq | |
| parent | 00a81f02a4433e8d5c770d99028ef53107bcbc72 (diff) | |
adjusting to new syntax.
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-abbrev.el | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 15302aeb..3a088c95 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -10,7 +10,7 @@ (define-abbrev-table 'coq-mode-abbrev-table '( ("a" "auto" holes-abbrev-complete 4) - ("ar" "autorewrite [ # ] using @{db}" holes-abbrev-complete 1) + ("ar" "autorewrite with @{db,db...} using @{tac}" holes-abbrev-complete 1) ("ab" "absurd " holes-abbrev-complete 0) ("abs" "absurd " holes-abbrev-complete 0) ("ap" "apply " holes-abbrev-complete 16) @@ -69,7 +69,7 @@ ("he" "Hint Extern @{cost} @{pat} => @{tac} : @{db}." holes-abbrev-complete 0) ("hi" "Hint Immediate # : @{db}." holes-abbrev-complete 0) ("hr" "Hint Resolve # : @{db}." holes-abbrev-complete 0) - ("hrw" "Hint Rewrite [#] in @{db} using @{tac}." holes-abbrev-complete 0) + ("hrw" "Hint Rewrite -> @{t1,t2...} using @{tac} : @{db}." holes-abbrev-complete 0) ("hs" "Hints # : #." holes-abbrev-complete 0) ("hu" "Hint Unfold # : #." holes-abbrev-complete 0) ("i" "intro " holes-abbrev-complete 10) |