search

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

Remove last use of omega. #94

Closed Zimmi48 closed 3 years ago

Zimmi48 commented 3 years ago

Compatibility with coq/coq#13741.

Untested.

Zimmi48 commented 3 years ago

@spitters It looks like this last call to omega cannot be replaced with a call to lia in version of Coq < 8.11 (it makes lia diverge). Are you opposed to dropping compatibility with Coq < 8.11?

spitters commented 3 years ago

Agreed!