diff options
| author | Emilio Jesus Gallego Arias | 2020-03-02 06:48:10 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-13 01:12:47 -0400 |
| commit | 1c744339e54d108f5cfcadd830431a27776a658f (patch) | |
| tree | 2d1b23fcb47c4b9896b7812893340f093a4120a3 /dev/base_include | |
| parent | b35dae7a6a9cc08c4bcdce7409e0ef45382b7ee1 (diff) | |
[lemmas] Consolidate some declaration data on Info.t
Now that `MutualEntry` provides a more uniform interface we can reuse
`Info.t`
In the medium term we shall consolidate `Proof` / `Proof_global` and
`Lemmas` so admitted / finish are uniform too.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions