MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_right

 In fact, this formula "fold ... = fold_right ... (rev (elements))"
 was already frequently used, but without ever stating it explicitely.
 Instead, we were always chaining two rewrites each time.

 Thanks to A. Appel for mentionning this question of fold_right vs.
 fold_left in the spec of fold.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14561 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions