aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/expl.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-04-16 14:49:25 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-04-16 14:49:25 -0400
commit6d021ead0f73c5a28080b50a1bd08b1ab72590c9 (patch)
tree1560f6013ce6de0388180550168c20e9756eaa2c /src/expl.sml
parent6d06bc0105d704373295c749aa65cc92488ac56c (diff)
Label exported symbols by effect-ness; factor out some common datatypes
Diffstat (limited to 'src/expl.sml')
-rw-r--r--src/expl.sml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/expl.sml b/src/expl.sml
index 859e21ff..e293c36b 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -70,7 +70,7 @@ datatype con' =
withtype con = con' located
-datatype datatype_kind = datatype Elab.datatype_kind
+datatype datatype_kind = datatype DatatypeKind.datatype_kind
datatype patCon =
PConVar of int