aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/iStream.mli
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-07-12 23:26:44 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-05-05 17:49:22 +0200
commit7e28feadd6394483b6f527d5aed7d663e189596e (patch)
tree9068e370691fa50b37668487268abcde0c0e430d /lib/iStream.mli
parentcff6f53cbef53ce3902e59853f7a7dc9b7150f45 (diff)
Upgrading some local function as a general-purpose combinator Option.List.map.
Diffstat (limited to 'lib/iStream.mli')
0 files changed, 0 insertions, 0 deletions