I am very curious about `Arith.Bool_nat`

. It's not required anywhere. What is it used for?

pretty common that Stdlib comprehension is going to require digital archeology. Your best bet might be to search the legacy Coq-contribs for `Bool_nat`

: https://github.com/coq-contribs/

for context, contribs contain probably a majority of all noteworthy Coq code written 1998-2011 or similar.

you can also search all github https://github.com/search?q=%22Bool_nat%22+language%3ACoq&type=code&l=Coq

I propose to deprecate it : https://github.com/coq/coq/pull/18538

One less file to take care of is still a little win.

Last updated: Oct 13 2024 at 01:02 UTC