aboutsummaryrefslogtreecommitdiff
path: root/catalog.ml
diff options
context:
space:
mode:
authorSébastien Dailly <sebastien@chimrod.com>2016-11-21 17:06:19 +0100
committerSébastien Dailly <sebastien@chimrod.com>2017-01-01 13:30:43 +0100
commit023c11470e32744a43b7e3c7c248f3c47ebdc687 (patch)
tree832e04c2923295d5adf61e58d9a333afb5b26c77 /catalog.ml
parentef312564ca84a2b49fc291434d8fb2f8501bb618 (diff)
Use gadt for function catalog
Diffstat (limited to 'catalog.ml')
0 files changed, 0 insertions, 0 deletions