Adapt to https://github.com/rocq-prover/rocq/pull/22124

[proux01]

Adapt to rocq-prover/rocq#22124

[jdchristensen]

I'm not sure why the current line or the new line are needed, but the new line seems to be a reasonable thing to have.

[jdchristensen]

This seems fine to me. I'll merge soon unless there are any other comments.

[proux01]

It's just a matter of printing style for case constructs: match _ with ... by default and if _ then ... for the specific case of boolean. There used to be a very generic if _ then _ construct for 2-constructor inductives (with printing triggered by Printing If) that we are on the way to deprecate for everything but bool (which will now only be identified by the given Register).

[jdchristensen]

It's just a matter of printing style for case constructs:

@proux01 Right, but I tested, and functions like andb print the same way with neither line in the file (using Rocq 9.1). So I don't know why we needed the Add Printing If Bool. line, and I'm not sure why the Register Bool as core.bool.type. line is needed. Maybe with the development branch it is needed to trigger the printing feature? Or is it an unrelated change? (But probably a useful one.)

[jdchristensen]

I guess you essentially already said that the register line will be needed to trigger the printing for bool in the future. Makes sense. Thanks!

[proux01]

Yes, the dev branch (i.e., the PR for which this is an overlay) needs both the removal of the Printing If and the Register (if one wants printing as if _ then _ rather than if _ is true then _).