diff options
| author | Emilio Jesus Gallego Arias | 2019-07-10 16:13:22 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-23 18:53:46 +0200 |
| commit | b6000bd57f9dd20858678caee7e3962081243694 (patch) | |
| tree | d327178793209000e46bfb23cb74cc5674b244ef /dev/ci | |
| parent | bbf2ded61869b8aa48e34424c15e795961820721 (diff) | |
[lemmas] save_remaining_recthms doesn't need a norm parameter.
We make the interface to this function simpler, as a step towards
trying to remove the duplication of this function with the code in
`DeclareDef`.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions