File mode specification error: (void-variable coq-cmd-force-next-proof-kept)

[DaKnig]

Steps to reproduce:

• package-install RET proof-general
• package-install RET company-coq
• open a coq file ending with .v
• get the error in the title

this error is reported again when re-enabling coq-mode

[DaKnig]

I did restart emacs a few times hoping the thing will solve itself , didnt help

[erikmd]

Hi @DaKnig, thanks for your report!

Could you give more details on your configuration? (OS and (if applicable) Linux distribution, emacs --version)

@hendriktews could you take a look? the reported error mentions the custom you had introduced in: https://github.com/ProofGeneral/PG/commit/0a793dbbe55c58348e581f828e77e651e195ed5d

[erikmd]

@DaKnig can you also run the following code and paste its output?

$ ls -dl ~/.emacs.d/elpa/proof-general-*

[hendriktews]

Can you retry without company-coq? I only see two occurrences of coq-cmd-force-next-proof-kept, one in coq.el and the declaration in coq-syntax.el. And coq.el loads coq-syntax.el. Therefore my suspicion is that the problem comes from copany-coq.

[hendriktews]

If you need a workaround, put

(setq coq-cmd-force-next-proof-kept "Let")

in your .emacs