diff options
| author | Emilio Jesus Gallego Arias | 2020-03-09 02:47:01 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 06:06:35 -0400 |
| commit | 8129fb2abce6ba2e5ddd1f384618bb2fb8f817b5 (patch) | |
| tree | 982db7b802ed407db6ac3bd967cb610b6b48f562 /doc/plugin_tutorial | |
| parent | a15e584571a4e153e98a11c93d12759c45ea2dcd (diff) | |
[proof] [mutual] Factorize mutual per-entry information
We move `Recthm` to `DeclareDef` so it is shared by interactive and
direct fixpoint declaration.
This is the last step before unifying both paths.
Diffstat (limited to 'doc/plugin_tutorial')
0 files changed, 0 insertions, 0 deletions