Rework of FMapAVL inspired by recent changes of FSetAVL:

 * pure functions comes first, proofs are isolated in a sub-module
 * lazy (&&&) = if ... then ... else true instead of strict (&&) = andb
 * equal and compare done via continuations
 * a more clever map2_opt suggested by B. Gregoire: no more 
    intermediate conversion to lists, some sub-functions can handle 
    trivial situations, etc.
 * map2 is now done via map2_opt and another new iterator: map_option.
   By the way, this map_option allows to define easily an efficient
   filter function. Both map2_opt and map_option are currently not 
   available through FMapInterface.S, but they can be used by direct
   reference to the underlying Raw module.



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

0 files changed, 0 insertions, 0 deletions