diff options
| author | ppedrot | 2012-12-08 16:23:32 +0000 |
|---|---|---|
| committer | ppedrot | 2012-12-08 16:23:32 +0000 |
| commit | c606c4870d492fc0b96b62368498227c3e4e5e86 (patch) | |
| tree | ecf0c89f41598d51ce9cbefdb7af7c6b6fb0c89c /lib | |
| parent | 0d5c92c80d14def48432093fc1ac94aae544c7fe (diff) | |
Small optimization in Closure: replaced an index list with an array.
This may consume more memory, but this should also be more efficient,
in particular when doing intensive computation. I get a ~2% speedup
on stdlib.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16047 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions