diff options
| author | Emilio Jesus Gallego Arias | 2019-08-19 23:43:55 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-08-23 23:41:08 +0200 |
| commit | 10b54c11e2db436ab077477fae862fe06e0d9395 (patch) | |
| tree | 3cd3892d568e1a9c71b883a638c25455ff62bc5d /kernel | |
| parent | b0a9cbeaf0530533008aa99246164b2bad896c5a (diff) | |
[lemmas] Cleanup users of default proof information.
We remove calls of `Lemmas.Info.make` that where using the default
parameters, as this is mostly dead code now.
This brings into question quite a few things, in particular, the
uneven support of `scope` attributes by different commands / plugins.
We don't attempt to solve that yet, hopefully the ongoing constant
saving path refactoring will be able to take care of these
inconsistencies.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions