diff options
| author | Emilio Jesus Gallego Arias | 2019-02-14 12:45:49 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-09 14:26:58 +0200 |
| commit | cb84805a1758ab52506f74207dacd80a8f07224e (patch) | |
| tree | 40b735ebbf6bde70df2ab8636a073b82262a4db2 /kernel/type_errors.mli | |
| parent | a8b3c907cb2d6da16bdeea10b943552dc9efc0ed (diff) | |
[save_proof] Make terminator API internal.
We refactor the terminator API to make it more internal. Indeed we
remove `set_terminator` and `get_terminator` is only there due to
access to internals in the STM `save_proof` path by the infamous
`?proof` parameter.
After this only 2 non-standard terminators remain: obligations and
derive. We will refactor those in next PRs.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions