diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-14 16:36:04 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-14 16:36:04 +0000 |
| commit | 25ba10c14d8771367fbda6efe8174e10769aa739 (patch) | |
| tree | 9e20d3a9467772a329b4fbc2cf0bc3f3de5ff4b1 /tools/coq_tex.ml4 | |
| parent | b57991c34dfc88820eee14e2962aa0833cbc3fe9 (diff) | |
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
Diffstat (limited to 'tools/coq_tex.ml4')
0 files changed, 0 insertions, 0 deletions