make compilation work for coq <= 8.10

coq-community / math-classes

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]

https://math-classes.github.io

MIT License

162 stars 43 forks source link

make compilation work for coq <= 8.10 #102

Closed larsr closed 3 years ago

larsr commented 3 years ago

On older coqc versions, lia will go into an infinite loop here if there is confusing stuff in the context. So we clean up the context a little in order to get backwards compatibility.

With this patch, different coq versions can use the same version of the math-classes library. It would for instance make obsolete this suggested patch to the nix-file https://github.com/NixOS/nixpkgs/pull/129766/commits/fdfbe8691fd75aaba4718fc9add8daa04dde3e5f

Zimmi48 commented 3 years ago

Should we restore compatibility testing with older versions?

spitters commented 3 years ago

Yes, why not?

Zimmi48 commented 3 years ago

Yeah, I also think it would be worthwhile, at least until we need to drop compatibility with old versions again. I will take care of this.

See #103