diff options
| author | Pierre Courtieu | 2005-03-08 17:08:28 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2005-03-08 17:08:28 +0000 |
| commit | 36ca763e45d4b4489983cd820b28a5d36cea04de (patch) | |
| tree | 512aac787488bcd698761260699e2c61160b022e /coq | |
| parent | 87af89b6acfaf48afc3166f10371bf6d190241f0 (diff) | |
small modifications, updating doc string of holes.el.
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-abbrev.el | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 29fc9b96..c73b4e4d 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -195,14 +195,14 @@ ) ("Notations" "COMMAND ABBREVIATION" - ["Infix inf<C-BS>" (holes-insert-and-expand "inf") t] - ["Notation (no assoc) nota<C-BS>" (holes-insert-and-expand "nota") t] - ["Notation (assoc) notas<C-BS>" (holes-insert-and-expand "notas") t] - ["Notation (no assoc, scope) notasc<C-BS>" (holes-insert-and-expand "notasc") t] - ["Notation (assoc, scope) notassc<C-BS>" (holes-insert-and-expand "notassc") t] - "" - ["Notation (simple) nots<C-BS>" (holes-insert-and-expand "nots") t] - ["Notation (simple,local) notsl<C-BS>" (holes-insert-and-expand "nots") t] + ["Infix inf<C-BS>" (holes-insert-and-expand "inf") t] + ["Notation (no assoc) nota<C-BS>" (holes-insert-and-expand "nota") t] + ["Notation (assoc) notas<C-BS>" (holes-insert-and-expand "notas") t] + ["Notation (no assoc, scope) notasc<C-BS>" (holes-insert-and-expand "notasc") t] + ["Notation (assoc, scope) notassc<C-BS>" (holes-insert-and-expand "notassc") t] + "" + ["Notation (simple) nots<C-BS>" (holes-insert-and-expand "nots") t] + ["Notation (simple,local) notsl<C-BS>" (holes-insert-and-expand "nots") t] ) ) |