diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2004-04-06 17:25:51 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2004-04-06 17:25:51 +0000 |
| commit | 57424b3cf8c3a901043b850adfed003e2f8c18b3 (patch) | |
| tree | c4afd923c2228a530a2349c7533c8c2e0e40a317 /coq | |
| parent | f560effab6f7242c88938f76782d56ba732c31a8 (diff) | |
added some commands in coq menu
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-abbrev.el | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 58e1d216..45828aeb 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -97,6 +97,9 @@ ("mo2" "Module # <: # := #." holes-abbrev-complete 0) ("moi" "Module # : #.\n#\nEnd #." holes-abbrev-complete 0) ("moi2" "Module # <: #.\n#\nEnd #." holes-abbrev-complete 0) + ("nots" "Notation # := #." holes-abbrev-complete 0) + ("notsl" "Notation Local # := #." holes-abbrev-complete 0) + ("not" "Notation \"#\" := # (at level #, # at level #)." holes-abbrev-complete 0) ("nota" "Notation \"#\" := # (at level #, # at level #)." holes-abbrev-complete 0) ("notas" "Notation \"#\" := # (at level #, # associativity)." holes-abbrev-complete 0) ("notasc" "Notation \"#\" := # (at level #, # at level #) : @{scope}." holes-abbrev-complete 0) @@ -193,6 +196,10 @@ ["Notation (assoc) notas<C-BS>" (insert-and-expand "notas") t] ["Notation (no assoc, scope) notasc<C-BS>" (insert-and-expand "notasc") t] ["Notation (assoc, scope) notassc<C-BS>" (insert-and-expand "notassc") t] + "" + ["Notation (simple) nots<C-BS>" (insert-and-expand "nots") t] + ["Notation (simple,local) notsl<C-BS>" (insert-and-expand "nots") t] + ) ) |