Addressing proposal #15562: cleaning API of functions for destructing/constructing abstractions or products wrt contexts

Kind: cleanup

Fixes / closes #15562

This organizes the naming of functions for destructing/constructing abstractions or products wrt contexts around the schemes "{decompose_,strip_,}{lam,prod}{_n,}{_assum,_decls,}{_red,}" and "dest{Lambda,Prod}{_red,}". See #15562 for details.

Better to merge #15453, #15524, #15565 first.

• [x] take a decision on possibly using hnf_ (like in hnf_prod_applist) rather than _red to mean that one reduces before looking for a binder.
• [x] keep old names with a deprecation notice? or at least document the changes
• [ ] goes one step further in uniformization and easiness to remember by using the radical lambda rather than lam (consistently with mkLambda, destLambda etc.)

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.

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

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.

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.

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.

Are there any dependencies left to merge?

Are there any dependencies left to merge?

No, I removed the label and rebased.

There was one last point to consider, namely to improve the symmetry with it_mk{Prod,Lambda,Prod_or_LetIn,...} by using the it_dest{Prod,Lambda,Prod_or_LetIn,...} pattern rather than the decompose_{prod,lambda,prod_decls,...} pattern. I don't know if developers are ready for this extra change.

@coqbot run full ci

@herbelin please link overlay PRs in the opening comment of this PR

Overlay link: done

@coqbot merge now

@SkySkimmer: Please take care of the following overlays:

• 15582-herbelin-master+cleaning-decompose_lam_n_assum-and-cie.sh