aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/himsg.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-19 01:35:00 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-19 01:35:00 +0000
commit051e8cec80025781de486a3884e9ff15cb17b7f5 (patch)
treed58178a1ee8804b4622facf0f5510e8303eb98c5 /toplevel/himsg.ml
parent489893c1ffc709023ada9c169106f2779919864a (diff)
Various improvements of coqdep, resulting in a big speedup
* use of Hashtbl for large sets/maps * reorganisation of directory-traversal functions, in order to avoid redundant stat / open * all files and directory whose names start by . are skipped while tranversing directories: no more visits of .svn ! * new option -boot to be used when computing dependencies of the stdlib: - no need in this case to records the system .vo in coqlibKnown - add directly inside coqdep the equivalent of -R theories Coq and -R contrib Coq As a result, coqdep'ing all the .vo of the stdlib now takes 25s on my machine instead of 2min30 earlier. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10695 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/himsg.ml')
0 files changed, 0 insertions, 0 deletions