Pierre-Yves Strub (Nov 10 2021 at 10:20): Pierre-Yves Strub (Nov 10 2021 at 10:20):Hi. With Coq 8.14 & PG 20211109.1442 (installed by elpa), I have this error when opening a Coq file:
File mode specification error: (coq-unclassifiable-version . 8.14.0 compiled)
Do you understand what is happening here?
Karl Palmskog (Nov 10 2021 at 10:21):probably related to this previous closed issue: https://github.com/ProofGeneral/PG/issues/600
Karl Palmskog (Nov 10 2021 at 10:21):ping @Erik Martin-Dorel
Pierre-Yves Strub (Nov 10 2021 at 10:24):Hmm. In fact, I was loading a old version of PG... This now works since the ELPA version is loaded. Sorry for the noise.
Karl Palmskog (Nov 10 2021 at 10:26):at least we find out that testing on Coq 8.14+rc1 paid off...
Last updated: Oct 13 2024 at 01:02 UTC