aboutsummaryrefslogtreecommitdiff
path: root/catalog.mli
diff options
context:
space:
mode:
authorSébastien Dailly <sebastien@chimrod.com>2016-11-15 13:00:01 +0100
committerSébastien Dailly <sebastien@chimrod.com>2016-11-15 13:00:01 +0100
commitef312564ca84a2b49fc291434d8fb2f8501bb618 (patch)
tree79415fcf225e6da1042c8edaae5e4a74c7a983cb /catalog.mli
Initial commit
Diffstat (limited to 'catalog.mli')
-rwxr-xr-xcatalog.mli4
1 files changed, 4 insertions, 0 deletions
diff --git a/catalog.mli b/catalog.mli
new file mode 100755
index 0000000..583db14
--- /dev/null
+++ b/catalog.mli
@@ -0,0 +1,4 @@
+
+val register: UTF8.t -> (ScTypes.types list -> ScTypes.types) -> unit
+
+val eval: UTF8.t -> ScTypes.types list -> ScTypes.types