category-theory icon indicating copy to clipboard operation
category-theory copied to clipboard

Published 20 hours ago • verified publisher icon jwiegley

Fix deprecation warnings

Open patrick-nicodemus opened this issue 8 months ago • 2 comments

Coq 8.19 deprecates the use of the % symbol in the Arguments command for managing scope, and advises to switch to %_. This PR implements this. This PR is not necessary to compile this library on Coq 8.20 or Rocq 9.0; it compiles without any failures. Coq 8.19 is the first Coq version to support the %_ operator in Arguments, so all the earlier versions will fail to build. Coq 8.19 was released in January 2024.

patrick-nicodemus avatar Mar 20 '25 15:03 patrick-nicodemus

I suppose now is the time to drop all support for Coq < 8.19?

jwiegley avatar Mar 21 '25 21:03 jwiegley

It's really not necessary because it compiles on Rocq 9.0 even without the changes. Users can silence the deprecation warning if they want. you can drop support for lower versions of Coq when this change becomes necessary.

patrick-nicodemus avatar Mar 21 '25 22:03 patrick-nicodemus