Where does proof-shell come from?

[tarsius]

I maintain the Emacsmirror and am once more tracking down unsatisfied dependencies.

This package requires proof-shell, which I assume should be provided by the coq package. However I cannot find a file proof-shell.el or a (provide 'proof-shell) anywhere else.

Could you please enlighten me? 😉

[cpitclaudel]

Yup, of course. It comes from Proof General, which just got added to MELPA, too! https://github.com/ProofGeneral/PG/blob/master/generic/proof-shell.el
Thanks for your tireless work and your dedication :)

[tarsius]

Thanks for the info.