diff --git a/modules/lang/lean/README.org b/modules/lang/lean/README.org index cf2f92fff..e12c17632 100644 --- a/modules/lang/lean/README.org +++ b/modules/lang/lean/README.org @@ -14,7 +14,6 @@ This module adds support for the [[https://leanprover.github.io/about/][Lean pro ** Packages - [[doom-package:lean-mode]] -- [[doom-package:company-lean]] if [[doom-module::completion company]] ** TODO Hacks #+begin_quote diff --git a/modules/lang/lean/config.el b/modules/lang/lean/config.el index d706630f3..70c984e2e 100644 --- a/modules/lang/lean/config.el +++ b/modules/lang/lean/config.el @@ -26,11 +26,3 @@ "h" #'lean-hole "m" #'lean-message-boxes-toggle "e" #'lean-execute)) - - -(use-package! company-lean - :when (modulep! :completion company) - :after lean-mode - :init - (advice-add #'company-lean-hook :override #'ignore) - (set-company-backend! 'lean-mode 'company-lean)) diff --git a/modules/lang/lean/packages.el b/modules/lang/lean/packages.el index 7a3640530..d4d415a96 100644 --- a/modules/lang/lean/packages.el +++ b/modules/lang/lean/packages.el @@ -2,6 +2,3 @@ ;;; lang/lean/packages.el (package! lean-mode :pin "99d6a34dc5b12f6e996e9217fa9f6fe4a6af037a") - -(when (modulep! :completion company) - (package! company-lean :pin "99d6a34dc5b12f6e996e9217fa9f6fe4a6af037a"))