From 0ce0b8071577f7edd546b1e12135021bdbfeac10 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Thu, 18 Mar 2004 10:21:16 +0000 Subject: adjusting to new syntax. --- coq/coq-abbrev.el | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'coq') 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) -- cgit v1.2.3