diff --git a/modules/lang/coq/config.el b/modules/lang/coq/config.el
index b44b58612..98b202787 100644
--- a/modules/lang/coq/config.el
+++ b/modules/lang/coq/config.el
@@ -1,16 +1,7 @@
 ;;; lang/coq/config.el -*- lexical-binding: t; -*-
 
 ;;;###package proof-general
-;; HACK `proof-general' ascertains its own library path at compile time in its
-;; autoloads file using `byte-compile-current-file' (and stores it in
-;; `pg-init--script-full-path'). This means that when
-;; `doom-package-autoload-file' is created and byte-compiled,
-;; `pg-init--script-full-path' will be wrong, causing file-missing errors as it
-;; tries to load `proof-site'. We prevent this by defining these two variables
-;; early, in our own autoloads file.
-(setq pg-init--script-full-path (locate-library "proof-general")
-      pg-init--pg-root (file-name-directory pg-init--script-full-path)
-      proof-splash-enable nil)
+(setq proof-splash-enable nil)
 
 
 ;;;###package coq
diff --git a/modules/lang/coq/packages.el b/modules/lang/coq/packages.el
index e10e63f3c..f51b087e9 100644
--- a/modules/lang/coq/packages.el
+++ b/modules/lang/coq/packages.el
@@ -1,6 +1,6 @@
 ;; -*- no-byte-compile: t; -*-
 ;;; lang/coq/packages.el
 
-(package! proof-general :pin "89829c25b9")
+(package! proof-general :pin "2a17093f6a")
 
 (package! company-coq :pin "6e8bc2e367")