From 57424b3cf8c3a901043b850adfed003e2f8c18b3 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 6 Apr 2004 17:25:51 +0000 Subject: added some commands in coq menu --- coq/coq-abbrev.el | 7 +++++++ 1 file changed, 7 insertions(+) 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" (insert-and-expand "notas") t] ["Notation (no assoc, scope) notasc" (insert-and-expand "notasc") t] ["Notation (assoc, scope) notassc" (insert-and-expand "notassc") t] + "" + ["Notation (simple) nots" (insert-and-expand "nots") t] + ["Notation (simple,local) notsl" (insert-and-expand "nots") t] + ) ) -- cgit v1.2.3