Improve warning for nonuniform coercions#17713

proux01 wants to merge 1 commit intorocq-prover:masterrocq-prover/rocq:masterfrom

proux01:advertize_nonuniform_optproux01/rocq:advertize_nonuniform_optCopy head branch name to clipboard