summaryrefslogtreecommitdiff
path: root/src/elab.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-08-14 18:35:08 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-08-14 18:35:08 -0400
commit7bdc4cabdb8e5efbc4a194fe0bfe9442c7644798 (patch)
treece4be93140bacbd8900ff57affd5f866fbbf3ad0 /src/elab.sml
parent5c9a5278b49ccf481468d5a766a8c4ab0cde2658 (diff)
Non-star SELECT
Diffstat (limited to 'src/elab.sml')
-rw-r--r--src/elab.sml4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/elab.sml b/src/elab.sml
index 66f5f3ed..9beff0c9 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -35,6 +35,7 @@ datatype kind' =
| KName
| KRecord of kind
| KUnit
+ | KTuple of kind list
| KError
| KUnif of ErrorMsg.span * string * kind option ref
@@ -66,6 +67,9 @@ datatype con' =
| CUnit
+ | CTuple of con list
+ | CProj of con * int
+
| CError
| CUnif of ErrorMsg.span * kind * string * con option ref