From b89fcd8726c8fa2ad9e2aab20bbbf67e8cf8f6a5 Mon Sep 17 00:00:00 2001 From: Sebastian Wild Date: Sat, 6 Oct 2018 23:45:09 +0200 Subject: [PATCH] Replace Coq-Mode abbreviations with yasnippet Since ProofGenerals abbreviation usage interfers with evil-mode, this empties the abbreviation table of coq-mode. The abbreviations got transformed into yasnippet snippets and put into hlissner/emacs-snippets#4. --- modules/lang/coq/README.org | 5 ++++- modules/lang/coq/config.el | 2 ++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/modules/lang/coq/README.org b/modules/lang/coq/README.org index 680555966..57459aa7e 100644 --- a/modules/lang/coq/README.org +++ b/modules/lang/coq/README.org @@ -1,3 +1,6 @@ #+TITLE: :lang coq -This module adds [[https://coq.inria.fr][coq]] support, powered by [[https://proofgeneral.github.io][Proof General]], with code completion via [[https://github.com/cpitclaudel/company-coq][company-coq]]. +This module adds [[https://coq.inria.fr][coq]] support, powered by [[https://proofgeneral.github.io][Proof General]]. + ++ Code completion ([[https://github.com/cpitclaudel/company-coq][company-coq]]) ++ [[https://github.com/hlissner/emacs-snippets/tree/master/coq-mode][Snippets]] diff --git a/modules/lang/coq/config.el b/modules/lang/coq/config.el index 1ff5cc560..eebd75636 100644 --- a/modules/lang/coq/config.el +++ b/modules/lang/coq/config.el @@ -3,6 +3,8 @@ ;; `coq' (setq proof-electric-terminator-enable t) +(setq coq-mode-abbrev-table '()) + (after! company-coq (set-lookup-handlers! 'company-coq-mode :definition #'company-coq-jump-to-definition