michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(lean-mode): remove 'annoying' abbreviations

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-26 14:50:10 -08:00
parent e55397d422
commit 4bee7554a3
1 changed files with 1 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/emacs/lean-mode.el
View file

@ -96,10 +96,7 @@
(local-set-key (kbd "TAB") 'lean-tab-indent-or-complete)) (local-set-key (kbd "TAB") 'lean-tab-indent-or-complete))
(define-abbrev-table 'lean-abbrev-table (define-abbrev-table 'lean-abbrev-table
'(("var" "variable") '())
("vars" "variables")
("def" "definition")
("th" "theorem")))
(defvar lean-mode-map (make-sparse-keymap) (defvar lean-mode-map (make-sparse-keymap)
"Keymap used in Lean mode") "Keymap used in Lean mode")