diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-04 12:17:57 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-04 12:17:57 +0000 |
| commit | a45a7f0411f19c10f7a50a02b84c1820c5907bb0 (patch) | |
| tree | 05254f5c8a7a34cc454a2b4bb160ba6bc18e1196 /dev | |
| parent | b021f265da7666fa93d34ae3e42fa8bcf28f63ac (diff) | |
Adding closure-preventing functions in CArray. These functions are all
higher-order functions like map and iter, and they are modified so that
they take one additional argument, thus saving a cloure allocation.
Compare the following.
Array.iter: ('a -> unit) -> 'a array -> unit
Array.Fun1.iter: ('r -> 'a -> unit) -> 'r -> 'a array -> unit
Basically, Array.Fun1.iter f x v = Array.iter (f x) v, though it does not
allocate a closure.
For now only the most critical functions are recoded.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17053 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions