search

coq-community / corn

Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
http://c-corn.github.io/
GNU General Public License v2.0
108 stars 43 forks source link

Adapt to Coq/Coq#18164 #202

Closed Villetaneuse closed 11 months ago

Villetaneuse commented 11 months ago

@VincentSe @spitters These are small modifications to deal with the removal of deprecated files in Arith.

spitters commented 11 months ago

@Villetaneuse Thanks. Can you fix the build issues on 8.15,8.14?

Villetaneuse commented 11 months ago

@Villetaneuse Thanks. Can you fix the build issues on 8.15,8.14?

Thank you. I'm trying. It might be ready tomorrow, but it's not that easy since many Set-decidable lemmas are missing.

Villetaneuse commented 11 months ago

@spitters This is now compatible with 8.14. I had to add a version of Nat.Even_Odd_dec in CLogic. You'll want to change CLogic.Even_Odd_dec with Nat.Even_Odd_dec (and remove CLogic.Even_Odd_dec) once the minimal version is bumped to 8.16.

Villetaneuse commented 11 months ago

Thanks!