So I've played around with
v8.12 for a while now. One in my mind quite big difference is that, when I try load .vo files that were compiled with another version of Coq (say, 8.11.2) I get a message along the lines of: "File.vo is corrupted" and nothing else.
This is very different from 8.11.2 and all previous versions, which were very specific about what the problem was, and talked about (something like) "File.vo signature was v8.10, expected v8.11". Is this an intentional change? I can get the exact error messages if there is interest.
The fix has just been merged (https://github.com/coq/coq/pull/12677)
thanks, was hard to know what to look for.
Last updated: Oct 15 2021 at 19:03 UTC