aboutsummaryrefslogtreecommitdiff
path: root/dev/base_include
diff options
context:
space:
mode:
authorThéo Zimmermann2017-05-16 18:28:41 +0200
committerThéo Zimmermann2017-05-16 18:28:41 +0200
commit530ce019b7bdcc2603027082f6b3f6841d5990e1 (patch)
treecabc0bd3f442df9a7229bff8dd9edd964d342a0f /dev/base_include
parent9f8220164703aee47c6c6d7dba07caabf7555c1c (diff)
Stop using auto with * in two proofs.
auto with * is an overkill for people who do not care to understand what they really need. In these two cases, one lemma which was available in the typeclass_instances hint db.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions