[bug#51755] [PATCH 0/1] Fix ProofGeneral (emacs front-end for Coq)

[zimoun]

Hi,

This is a follow-up of bug#46016 [1] and I think close it.

Now, it is possible to use ProofGeneral as any other Emacs packages.  For
instance,

   guix shell emacs proof-general coq
   emacs foo.v

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 [2]).

Cheers,
simon



1: <http://issues.guix.gnu.org/issue/46016>
2: 
<https://proofgeneral.github.io/doc/master/userman/Introducing-Proof-General/#Supported-proof-assistants>


zimoun (1):
  gnu: proof-general: Adjust autoloads for Emacs.

 gnu/packages/coq.scm | 85 +++++++++++++++++++++++---------------------
 1 file changed, 45 insertions(+), 40 deletions(-)


base-commit: 140b486437670ce95cb24a935b58cba52a9dac31
-- 
2.33.1