diff options
| author | Pierre-Marie Pédrot | 2017-12-13 10:42:41 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-12-30 19:19:03 +0100 |
| commit | c73fa639eb0a8eaf4e5121aa600f88f2d4349a0c (patch) | |
| tree | 995ef76564fb951d0dd84a5834d05bbe27b5d239 /kernel/mod_typing.ml | |
| parent | 2d6e395dead61a49ede6208bc40e16b4b8e68ce4 (diff) | |
Using a dedicated type for Lib.abstr_info.
Diffstat (limited to 'kernel/mod_typing.ml')
0 files changed, 0 insertions, 0 deletions