summaryrefslogtreecommitdiff
path: root/src/main.ml
diff options
context:
space:
mode:
authorGabriel Kerneis2013-08-19 17:16:51 +0100
committerGabriel Kerneis2013-08-19 17:16:51 +0100
commit797cefdfd99d9b5ee4a1f619610b5bb52692f443 (patch)
tree1854bcf270587c8167d6fc3994ab028bfd9a9733 /src/main.ml
parent0372f89b3a4d805b3cfdb7910eb6206e1e2133a2 (diff)
language.ott: syntax for types in patterns
Diffstat (limited to 'src/main.ml')
0 files changed, 0 insertions, 0 deletions