diff options
| author | Emilio Jesus Gallego Arias | 2020-05-22 03:55:40 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-26 18:26:47 +0200 |
| commit | 946c6c7e58a1dfbe57445a0a1508a587193bb7c3 (patch) | |
| tree | d5deba68d2f2cba0d0497233538b397924571898 /doc/plugin_tutorial | |
| parent | 1eb5f0504561224affd93717a9fca0e3162dcdd9 (diff) | |
[declare] Simplify exported type of definition_entry
This reduces the amount of exported internals, in particular
w.r.t. proof delaying and side effects which we will need in future
refactorings.
Actually turning the type from `Evd.side_effects proof_entry` to `unit
proof_entry` is left for the next commits.
Diffstat (limited to 'doc/plugin_tutorial')
0 files changed, 0 insertions, 0 deletions