diff --git a/modules/lang/coq/config.el b/modules/lang/coq/config.el
index a8a600663..62bbe97fe 100644
--- a/modules/lang/coq/config.el
+++ b/modules/lang/coq/config.el
@@ -1,8 +1,5 @@
 ;;; lang/coq/config.el -*- lexical-binding: t; -*-
 
-;; set this to the absolute path of the folder containing proof-site.el, e.g. /home/$USER/GitHub/PG/generic
-(defvar +coq-pg-loc nil)
-
 (def-package! proof-site
   :load-path +coq-pg-loc
   :defer t
diff --git a/modules/lang/coq/packages.el b/modules/lang/coq/packages.el
index d813083d3..3ae652118 100644
--- a/modules/lang/coq/packages.el
+++ b/modules/lang/coq/packages.el
@@ -1,4 +1,6 @@
 ;; -*- no-byte-compile: t; -*-
 ;;; lang/coq/packages.el
 
+(package! proof-general :recipe (:fetcher github :repo "ProofGeneral/PG" :files ("*")))
+
 (package! company-coq)