diff options
| author | Emilio Jesus Gallego Arias | 2020-03-13 06:46:47 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-30 19:05:36 -0400 |
| commit | 76115e703751cfde99d7e86be9eea8fb32398e8a (patch) | |
| tree | 921df7b0e82e8681167adecc4561876489ab53e2 /doc/plugin_tutorial/tuto1 | |
| parent | 07a0ec4416fae0f98c610752bc73a30a30f1bd64 (diff) | |
[lemmas] Cleanup in handling of mutual definitions
This is a tiny step towards making the code closer to its counterpart
in `DeclareDef`.
Diffstat (limited to 'doc/plugin_tutorial/tuto1')
0 files changed, 0 insertions, 0 deletions