summaryrefslogtreecommitdiff
path: root/src/expl.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-11-06 10:43:48 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-11-06 10:43:48 -0500
commitea5a24773259c147e806960843d3305a3c72067b (patch)
tree2e714f5fc0b6c669bad6c201f3a4b11fec490513 /src/expl.sml
parent12bb99a0ba702af12e89bfe544f2a572e5d4818d (diff)
Cookies through explify
Diffstat (limited to 'src/expl.sml')
-rw-r--r--src/expl.sml3
1 files changed, 1 insertions, 2 deletions
diff --git a/src/expl.sml b/src/expl.sml
index 8f531516..57396684 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -110,8 +110,6 @@ datatype sgn_item' =
| SgiVal of string * int * con
| SgiSgn of string * int * sgn
| SgiStr of string * int * sgn
- | SgiTable of int * string * int * con
- | SgiSequence of int * string * int
and sgn' =
SgnConst of sgn_item list
@@ -136,6 +134,7 @@ datatype decl' =
| DTable of int * string * int * con
| DSequence of int * string * int
| DDatabase of string
+ | DCookie of int * string * int * con
and str' =
StrConst of decl list