diff --git a/modules/lang/coq/README.org b/modules/lang/coq/README.org
new file mode 100644
index 000000000..680555966
--- /dev/null
+++ b/modules/lang/coq/README.org
@@ -0,0 +1,3 @@
+#+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]].
diff --git a/modules/lang/coq/autoload.el b/modules/lang/coq/autoload.el
new file mode 100644
index 000000000..624185018
--- /dev/null
+++ b/modules/lang/coq/autoload.el
@@ -0,0 +1,4 @@
+;;; lang/coq/autoload.el -*- lexical-binding: t; -*-
+
+;;;###autoload
+(add-hook 'coq-mode-hook #'company-coq-mode)
diff --git a/modules/lang/coq/packages.el b/modules/lang/coq/packages.el
new file mode 100644
index 000000000..3ae652118
--- /dev/null
+++ b/modules/lang/coq/packages.el
@@ -0,0 +1,6 @@
+;; -*- no-byte-compile: t; -*-
+;;; lang/coq/packages.el
+
+(package! proof-general :recipe (:fetcher github :repo "ProofGeneral/PG" :files ("*")))
+
+(package! company-coq)