This is a follow-up of bug#46016  and I think close it.
Now, it is possible to use ProofGeneral as any other Emacs packages. For
guix shell emacs proof-general coq
For now, the dependency of 'coq' is removed as with many Emacs packages.
Other said, the user has to provide such dependency. IMHO, it is the spirit
of such package where the 'prover' is let to the user (several are more or
less supported, see doc ).
gnu: proof-general: Adjust autoloads for Emacs.
gnu/packages/coq.scm | 85 +++++++++++++++++++++++---------------------
1 file changed, 45 insertions(+), 40 deletions(-)