Now Ring does not perform any more the same reduction twice. This was a logical bug of the sort_subterm function, in the sense that the aim of the function (as stated in the comment) was not to make early reductions mess with subterms; what happened, though, was that the first reduction completely removed the term and the second reduction became completely dummy.
Now Ring does not perform any more the same reduction twice.
This was a logical bug of the sort_subterm function, in the
sense that the aim of the function (as stated in the comment)
was not to make early reductions mess with subterms; what
happened, though, was that the first reduction completely
removed the term and the second reduction became completely
dummy.


git-svn-id: 44dc50bdcc0f5d1a212c497508dc9452e0b35e2b@1247 85f007b7-540e-0410-9357-904b9bb8a0f7

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