search

math-comp / hierarchy-builder

High level commands to declare a hierarchy based on packed classes
MIT License
95 stars 20 forks source link

Please fix test for Coq 8.20 #399

Closed SkySkimmer closed 9 months ago

SkySkimmer commented 9 months ago

https://github.com/math-comp/hierarchy-builder/blob/coq-master/tests/infer.v#L20

CohenCyril commented 9 months ago

@SkySkimmer could expand? Do you mean we should add a CI entry for Coq 8.20?

SkySkimmer commented 9 months ago

Sorry, I posted the wrong link. Edited to https://github.com/math-comp/hierarchy-builder/blob/coq-master/tests/infer.v#L20

SkySkimmer commented 9 months ago

master branch needs to be updated (and coq-master should probably be deleted to reduce confusion) cf https://github.com/coq/coq/pull/17722#discussion_r1314990614 https://github.com/math-comp/hierarchy-builder/pull/381#issuecomment-1697253073)