record of current timings

    time make topten
    "coqdep" -c -R . Ktheory "Utilities.v" > "Utilities.v.d" || ( RV=$?; rm -f "Utilities.v.d"; exit ${RV} )
    "coqdep" -c -R . Ktheory "Categories.v" > "Categories.v.d" || ( RV=$?; rm -f "Categories.v.d"; exit ${RV} )
    : compiling Utilities.v ; >Utilities.timing \time -f "%U sec, %M bytes: Utilities" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -time  Utilities
    0.11 sec, 430194688 bytes: Utilities
    : compiling Categories.v ; >Categories.timing \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -time  Categories
    1.81 sec, 1372389376 bytes: Categories
    ./Categories.v:38189-38197: [Defined.] 0.403 secs (0.403u,0.s)
    ./Categories.v:38047-38184: [exact~~(Abgr.Product.UniqueMap...] 0.289 secs (0.288u,0.s)
    ./Categories.v:20244-20248: [Qed.] 0.115 secs (0.114u,0.s)
    ./Categories.v:38018-38040: [apply~El.mor_equality.] 0.057 secs (0.057u,0.s)
    ./Categories.v:20156-20175: [apply~mor_equality.] 0.038 secs (0.038u,0.s)
    ./Categories.v:17094-17117: [End~StandardCategories.] 0.036 secs (0.031u,0.004s)
    ./Categories.v:37874-37912: [exists~(Abgr.Product.Map~X~T_o...] 0.034 secs (0.034u,0.s)
    ./Categories.v:20204-20223: [apply~mor_equality.] 0.034 secs (0.034u,0.s)
    ./Categories.v:37839-37865: [destruct~T~as~(T_ob,~T_el).] 0.029 secs (0.029u,0.s)
    ./Categories.v:19706-19742: [intros~?~?~(c,~x)~(d,~y)~(f,~i...] 0.025 secs (0.025u,0.s)

    real	0m2.273s
    user	0m1.998s
    sys	0m0.262s