diff --git a/modules/lang/coq/autoload.el b/modules/lang/coq/autoload.el
index 390a3f94f..624185018 100644
--- a/modules/lang/coq/autoload.el
+++ b/modules/lang/coq/autoload.el
@@ -1,5 +1,4 @@
 ;;; lang/coq/autoload.el -*- lexical-binding: t; -*-
-;;;###if (featurep! :completion company)
 
 ;;;###autoload
 (add-hook 'coq-mode-hook #'company-coq-mode)
diff --git a/modules/lang/coq/config.el b/modules/lang/coq/config.el
new file mode 100644
index 000000000..1ff5cc560
--- /dev/null
+++ b/modules/lang/coq/config.el
@@ -0,0 +1,12 @@
+;;; lang/coq/config.el -*- lexical-binding: t; -*-
+
+;; `coq'
+(setq proof-electric-terminator-enable t)
+
+(after! company-coq
+  (set-lookup-handlers! 'company-coq-mode
+    :definition #'company-coq-jump-to-definition
+    :references #'company-coq-grep-symbol
+    :documentation #'company-coq-doc)
+  (unless (featurep! :completion company)
+    (setq company-coq-disabled-features '(company company-defaults))))
diff --git a/modules/lang/coq/packages.el b/modules/lang/coq/packages.el
index 69d5299b5..3ae652118 100644
--- a/modules/lang/coq/packages.el
+++ b/modules/lang/coq/packages.el
@@ -3,5 +3,4 @@
 
 (package! proof-general :recipe (:fetcher github :repo "ProofGeneral/PG" :files ("*")))
 
-(when (featurep! :completion company)
-  (package! company-coq))
+(package! company-coq)