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