diff options
| author | Théo Zimmermann | 2017-05-16 18:28:41 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2017-05-16 18:28:41 +0200 |
| commit | 530ce019b7bdcc2603027082f6b3f6841d5990e1 (patch) | |
| tree | cabc0bd3f442df9a7229bff8dd9edd964d342a0f /kernel/cbytecodes.ml | |
| parent | 9f8220164703aee47c6c6d7dba07caabf7555c1c (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 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions