summaryrefslogtreecommitdiff
path: root/src/elab.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-06-17 16:38:54 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-06-17 16:38:54 -0400
commitb9406323848c150f5a8562ad206916c446529d65 (patch)
tree5464b011b61ca366be29dabd74275245b60659b9 /src/elab.sml
parent4bb0bbc1920b5474619cb00e278590e029cdb12a (diff)
Elaborating module projection
Diffstat (limited to 'src/elab.sml')
-rw-r--r--src/elab.sml3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/elab.sml b/src/elab.sml
index 14664c0f..da64febf 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -51,6 +51,7 @@ datatype con' =
| CRel of int
| CNamed of int
+ | CModProj of int * string list * string
| CApp of con * con
| CAbs of string * kind * con
@@ -68,6 +69,7 @@ datatype exp' =
EPrim of Prim.t
| ERel of int
| ENamed of int
+ | EModProj of int * string list * string
| EApp of exp * exp
| EAbs of string * con * con * exp
| ECApp of exp * con
@@ -103,6 +105,7 @@ datatype decl' =
and str' =
StrConst of decl list
| StrVar of int
+ | StrProj of str * string
| StrError
withtype decl = decl' located