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

[zimoun]

Hi Coq or Emacs reviewers,

On Wed, 10 Nov 2021 at 20:26, zimoun <zimon.toutoune@gmail.com> wrote:

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

Friendly ping. :-)


Cheers,
simon