diff options
| author | Daniel de Rauglaudre | 2016-04-08 14:53:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-08 14:58:42 +0200 |
| commit | 17c9a9775e99d1551bf6d346d731271e3ae34417 (patch) | |
| tree | 04c63b6dded7381b61a8d915fd486744967efefd /dev/base_include | |
| parent | 9f0a896536e709880de5ba638069dea680803f62 (diff) | |
Fixing a source of inefficiency and an artificial dependency in the
printer in the congruence tactic.
Debugging messages were always built even when not in the verbose mode
of congruence.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions