Fix coercion code to disallow using cumulativity in the domain of products, which results in strange changes in user provided terms.
Fix coercion code to disallow using cumulativity in the domain of products, which
results in strange changes in user provided terms.

mlasson/coq,silene/coq,maximedenes/coq,ppedrot/coq,pirapira/coq2rust,asr/coq,Matafou/coq,maximedenes/coq,asr/coq,TheTypoMaster/coq,Zimmi48/coq,jpdeplaix/coq,Ptival/coq,SkySkimmer/coq,JasonGross/coq,SkySkimmer/coq,asr/coq,letouzey/coq-wip,ppedrot/coq,gmalecha/coq,mattam82/coq,TheTypoMaster/coq,Zimmi48/coq,letouzey/coq-wip,JasonGross/coq,gares/coq,Ptival/coq,aspiwack/coq,gares/coq,Zimmi48/coq,coq/coq,aspiwack/coq,gares/coq,silene/coq,ppedrot/coq,ppedrot/coq,Lionel-Rieg/coq,pirapira/coq2rust,barras/coq,aspiwack/coq,mattam82/coq,gmalecha/coq,ejgallego/coq,barras/coq,gares/coq,coq/coq,coq/coq,TheTypoMaster/coq,8l/coq,Ptival/coq,amintimany/coq,maximedenes/coq,amintimany/coq,SkySkimmer/coq,ale-f/coq,Matafou/coq,william-lawvere/coq,gmalecha/coq,william-lawvere/coq,JasonGross/coq,mattam82/coq,ejgallego/coq,ppedrot/coq,letouzey/coq-wip,Lionel-Rieg/coq,william-lawvere/coq,TOSPIO/coq,jpdeplaix/coq,gares/coq,JasonGross/coq,Matafou/coq,SkySkimmer/coq,letouzey/coq-wip,ejgallego/coq,TOSPIO/coq,barras/coq,shindere/coq,shindere/coq,Lionel-Rieg/coq,coq/coq,shindere/coq,Zimmi48/coq,ale-f/coq,mlasson/coq,maximedenes/coq,herbelin/github-coq,silene/coq,8l/coq,ejgallego/coq,letouzey/coq-wip,mlasson/coq,amintimany/coq,TOSPIO/coq,pirapira/coq2rust,8l/coq,maximedenes/coq,herbelin/github-coq,ale-f/coq,herbelin/github-coq,jpdeplaix/coq