From dbefcc58687d1fabb8df030f2308e97fff781d47 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 16 Mar 2004 16:35:31 +0000 Subject: Added 'Notation' stuff to coq menu command insert. --- coq/coq-abbrev.el | 4 ++++ 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) diff --git a/coq/coq.el b/coq/coq.el index 57c1836a..0886799f 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -116,14 +116,17 @@ ["Functional Scheme fs" (insert-and-expand "fs") t] ["Functional Scheme with fsw" (insert-and-expand "fsw") t] "" - ["hint Constructors hc" (insert-and-expand "hc") t] - ["hint Immediate hi" (insert-and-expand "hi") t] - ["hint Resolve hr" (insert-and-expand "hr") t] - ["hint Rewrite hrw" (insert-and-expand "hrw") t] - ["hint extern he" (insert-and-expand "he") t] - ["hints hs" (insert-and-expand "hs") t] + ["Hint Constructors hc" (insert-and-expand "hc") t] + ["Hint Immediate hi" (insert-and-expand "hi") t] + ["Hint Resolve hr" (insert-and-expand "hr") t] + ["Hint Rewrite hrw" (insert-and-expand "hrw") t] + ["Hint Extern he" (insert-and-expand "he") t] "" ["infix inf" (insert-and-expand "inf") t] + ["Notation (no assoc) nota" (insert-and-expand "nota") t] + ["Notation (assoc) notas" (insert-and-expand "notas") t] + ["Notation (no assoc, scope) notasc" (insert-and-expand "notasc") t] + ["Notation (assoc, scope) notassc" (insert-and-expand "notassc") t] ) ("Insert term" -- cgit v1.2.3