aboutsummaryrefslogtreecommitdiff
path: root/catalog.mli
diff options
context:
space:
mode:
authorSébastien Dailly <sebastien@chimrod.com>2017-11-01 14:53:09 +0100
committerSébastien Dailly <sebastien@chimrod.com>2017-11-01 14:53:09 +0100
commit9fbc5e48ea8183dda8fdb652364c0c29f8a309d5 (patch)
tree052214454101b44d07918131ad500f0c451649eb /catalog.mli
parentab721136f50914a21f6cca89f0fcfb055ba58cd2 (diff)
Made scTypes.types private.
Diffstat (limited to 'catalog.mli')
0 files changed, 0 insertions, 0 deletions