diff options
| -rw-r--r-- | coq/coq-abbrev.el | 4 | ||||
| -rw-r--r-- | coq/coq.el | 15 |
2 files changed, 13 insertions, 6 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 658b81d1..6d9a097e 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -100,6 +100,10 @@ ("mo2" "Module # <: # := #." holes-abbrev-complete 0) ("moi" "Module # : #.\n#\nEnd #." holes-abbrev-complete 0) ("moi2" "Module # <: #.\n#\nEnd #." 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 #) : #." holes-abbrev-complete 0) + ("notassc" "Notation \"#\" := # (at level #, # associativity) : #." holes-abbrev-complete 0) ("o" "omega" holes-abbrev-complete 0) ("om" "Omega" holes-abbrev-complete 0) ("p" "Print #" holes-abbrev-complete 3) @@ -116,14 +116,17 @@ ["Functional Scheme fs<C-BS>" (insert-and-expand "fs") t] ["Functional Scheme with fsw<C-BS>" (insert-and-expand "fsw") t] "" - ["hint Constructors hc<C-BS>" (insert-and-expand "hc") t] - ["hint Immediate hi<C-BS>" (insert-and-expand "hi") t] - ["hint Resolve hr<C-BS>" (insert-and-expand "hr") t] - ["hint Rewrite hrw<C-BS>" (insert-and-expand "hrw") t] - ["hint extern he<C-BS>" (insert-and-expand "he") t] - ["hints hs<C-BS>" (insert-and-expand "hs") t] + ["Hint Constructors hc<C-BS>" (insert-and-expand "hc") t] + ["Hint Immediate hi<C-BS>" (insert-and-expand "hi") t] + ["Hint Resolve hr<C-BS>" (insert-and-expand "hr") t] + ["Hint Rewrite hrw<C-BS>" (insert-and-expand "hrw") t] + ["Hint Extern he<C-BS>" (insert-and-expand "he") t] "" ["infix inf<C-BS>" (insert-and-expand "inf") t] + ["Notation (no assoc) nota<C-BS>" (insert-and-expand "nota") t] + ["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] ) ("Insert term" |