diff options
| author | Pierre-Marie Pédrot | 2019-12-09 21:48:12 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-09 22:03:32 +0100 |
| commit | 7943acfd346466b512eca88fd32c738cdfe44299 (patch) | |
| tree | 66ff0cacd3258cd626be7aa5d80250105ca7d67e /kernel/indTyping.ml | |
| parent | 675579e23be006e2d545f1f458baf7a0f6b5883a (diff) | |
Type-safe implementation of libobjects.
Same justification as the change in implementation of Summary.
Diffstat (limited to 'kernel/indTyping.ml')
0 files changed, 0 insertions, 0 deletions