diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2004-03-16 16:35:31 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2004-03-16 16:35:31 +0000 |
| commit | dbefcc58687d1fabb8df030f2308e97fff781d47 (patch) | |
| tree | e3a9602dc4d96750c0936576e5098a108b5d5f64 /coq/coq-abbrev.el | |
| parent | 198afc029bad97919e10ade53d49122ca0eb7c7b (diff) | |
Added 'Notation' stuff to coq menu command insert.
Diffstat (limited to 'coq/coq-abbrev.el')
| -rw-r--r-- | coq/coq-abbrev.el | 4 |
1 files changed, 4 insertions, 0 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) |