diff options
| author | Emilio Jesus Gallego Arias | 2020-06-18 20:14:19 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-26 14:38:12 +0200 |
| commit | c7a62d0ee0205dfe5bef4bb874c04f1978d4b5c3 (patch) | |
| tree | bbd20c6801c5d7e885759ef31df51a3eaa030027 /kernel/type_errors.ml | |
| parent | 22bb101bae56a56a7bcdad2562daf5150ee9408b (diff) | |
[declare] Refactor analysis and construction of mutual lemmas
When declaring a lemma, the code path is quite different depending on
whether the lemma is inferred to be a mutually-defined lemma or not.
We refactor the code path in declare to reflect that; this will allow
to better organize constant information and to reuse the `Recthm.t`
type in particular.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions