diff options
| author | Pierre-Marie Pédrot | 2019-12-09 18:50:47 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-09 22:03:32 +0100 |
| commit | 675579e23be006e2d545f1f458baf7a0f6b5883a (patch) | |
| tree | b64df09a97ed484d7e03e49ea818e49123ed712f /library/libobject.ml | |
| parent | f00ad3178990c84c5169e4e86bb9a65dbfd539ff (diff) | |
Simplify the implementation of Summary by specifying the type of ML-MODULES.
No need to deploy an existential type machinery when we already know this type
in advance.
Diffstat (limited to 'library/libobject.ml')
0 files changed, 0 insertions, 0 deletions