I searched for such lemmas using Search headconcl:sumbool.

Among the results, I did not changed the following lemmas:

• lemmas about reals (e.g. Rle_lt_dec) that do not compute anyway as far as I can tell;
• lemmas about excluded middle (e.g. constructive_definite_descr_excluded_middle) for the same reason;
• lemma Zmin_le_prime_inf which is in a deprecated file.

Not sure what should be done w.r.t. test-suite/documentation/changelog.

Ping. The commit itself is fairly trivial, it is more a political question of deciding whether these lemmas must be made transparent. Not sure if this is acceptable for 8.14.

Regardless of what is implemented in this PR, I think we should have a more principled approach to the opacity problem, and in particular a set of systematic guidelines for the standard library. This issue has been popping regularly and we should tackle it once and for all instead of haphazardly making things defined.

I think that most of the issues can be summarized as a phase boundary between Prop and Type, so we should probably take singleton elimination as a guiding principle.

• Falsity is fine because it does not matter for computation.
• Equalities over decidable types can be made to compute by wrapping them in a transparent decider so there is not real point in making them transparent.
• Generic equalities are more tricky, which is something that should be decided carefully.
• Accessibility proofs block computations, but for practical purposes they can be eta-expanded by a huge factor through a combinator to not be problematic in practice. This is similar to equality canonization.

In this PR, the equality subproofs of the sumbool are indistinctively set transparent, while I believe that per the above verbiage, only the computational skeleton should be exposed, the (dis)equality subproofs should probably be Qed-opaque.

I tried to have a global approach, and that's why I dealt with all the sumbool lemmas instead of just NoDup_decand incl_dec, but I understand that you're speaking of an approach even more global.

As for the proofs, I considered that what was important was to compute the head constructor (regardless of the proposition inside the sumbool, which is somewhat arbitrary, but allows to use if then else effectively). From this point of view, only left and right in the proof should be exposed, the rest can be turned opaque. But since the proofs were small, I took the simpler approach of making the whole proof transparent. By the way, I wonder what is the typical way of making only some parts of a proof opaque. For me, the basic tool is abstract, but as I read that this tactics also has drawbacks, I am not sure if this is the recommended approach.

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

@coq/stdlib-maintainers should we resurrect and make progress on this PR?

I agree with @ppedrot that while the need is there, the way it is done is not very agreeable. Besides the arguments he gave I would say that transparent definitions should be stable and not be defined with tactics like auto. Frequently proofs depend on the exact definition. This goes together with @ppedrot's recommendation to to split the definition in the purely computational part and opaque lemmas for the Prop part.

This PR was not rebased after 30 days despite the warning, it is now closed.