two more timing results

=============================================================================
make SHARING=no
: compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -verbose  Categories
...
{
destruct T as [T_ob T_el].
exists (Mor X T_ob T_el).
simpl.
apply funextsec.
Time (
            let x := constr:(Eqn X T_ob T_el) in
            let T := type of x in
            change T
          ).
Finished transaction in 2.335 secs (2.331u,0.002s)
Time Timeout 50 exact (Eqn X T_ob T_el).
Finished transaction in 0.004 secs (0.004u,0.s)
}
admit.
Time Defined.
Finished transaction in 2.441 secs (2.438u,0.002s)
End Product.
End Ab.
6.00 sec, 1405435904 bytes: Categories
=============================================================================
make SHARING=no
: compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -verbose  Categories
...
{
destruct T as [T_ob T_el].
exists (Mor X T_ob T_el).
simpl.
apply funextsec.
Time (
            let x := constr:(Eqn X T_ob T_el) in
            let T := type of x in
            change T
          ).
Finished transaction in 2.313 secs (2.311u,0.002s)
Time admit.
Finished transaction in 0.007 secs (0.007u,0.s)
}
admit.
Time Defined.
Finished transaction in 2.411 secs (2.408u,0.002s)
End Product.
End Ab.
5.92 sec, 1407991808 bytes: Categories
=============================================================================