deprecate prod_curry and prod_uncurry

[liyishuai]

Per https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/prod_curry.2Funcurry.20seem.20named.20backward

Kind: feature.

• Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).

[Blaisorblade]

Cool, thanks! Follow-up: Can a library be compatible with older Coqs, use these functions and avoid triggering warnings?

[liyishuai]

Can a library be compatible with older Coqs, use these functions and avoid triggering warnings?

I know Java has @SuppressWarnings("deprecation"), maybe worth a Coq equivalent?

[Zimmi48]

Yes, you should use Set Warnings "-foo". where foo is either the warning name or the warning category. You can also add Set Warnings "foo". afterwards to reactivate the warning for the rest of the file.

[anton-trunov]

CI keeps failing for this PR. Can something be done here? Maybe a rebase would help if it has already been fixed on master?

[liyishuai]

CI seems happy now.