| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
adding size as static argument in quickcheck_narrowing compilation
|
changeset |
files
|
| Sun, 20 Mar 2011 23:07:06 +0100 |
wenzelm |
modernized specifications;
|
changeset |
files
|
| Sun, 20 Mar 2011 22:48:08 +0100 |
wenzelm |
dropped unused structure aliases;
|
changeset |
files
|
| Sun, 20 Mar 2011 22:47:08 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 20 Mar 2011 22:26:43 +0100 |
wenzelm |
NEWS: structure Timing provides various operations for timing;
|
changeset |
files
|
| Sun, 20 Mar 2011 22:08:12 +0100 |
wenzelm |
simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
|
changeset |
files
|
| Sun, 20 Mar 2011 21:44:38 +0100 |
wenzelm |
pure Timing.timing, without any exception handling;
|
changeset |
files
|
| Sun, 20 Mar 2011 21:28:11 +0100 |
wenzelm |
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
|
changeset |
files
|
| Sun, 20 Mar 2011 21:20:07 +0100 |
wenzelm |
pervasive cond_timeit;
|
changeset |
files
|
| Sun, 20 Mar 2011 20:20:41 +0100 |
wenzelm |
eliminated dead code;
|
changeset |
files
|
| Sun, 20 Mar 2011 20:05:43 +0100 |
wenzelm |
parallel preparation of document variants, within separate directories;
|
changeset |
files
|
| Sun, 20 Mar 2011 19:47:26 +0100 |
wenzelm |
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
|
changeset |
files
|
| Sun, 20 Mar 2011 19:34:18 +0100 |
wenzelm |
eliminated redundant doc_prefix1;
|
changeset |
files
|
| Sun, 20 Mar 2011 19:10:09 +0100 |
wenzelm |
renamed doc_prefix2 to dump_prefix;
|
changeset |
files
|
| Sun, 20 Mar 2011 18:56:36 +0100 |
wenzelm |
tuned;
|
changeset |
files
|