diff options
| author | Hugo Herbelin | 2016-09-01 09:59:20 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-09-01 10:00:47 +0200 |
| commit | 18046e2525300b990db4c8817f1cc02dcab97445 (patch) | |
| tree | c8e7109616e252ebecedc42097ddae6f6ed15751 /stm/asyncTaskQueue.ml | |
| parent | 7d4b8108bc8fa6951e605cb9b42580ff6f8e583f (diff) | |
Moving log of "TacReduce"/"reduce" to Tactics.reduce so that internal
calls are logged too. Using appropriate printer for reparsability of
the output.
Diffstat (limited to 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions