aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/source.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2012-04-29 13:17:31 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2012-04-29 13:17:31 -0400
commit05b7d79819dd5f006527bef7679b06868b3e0da7 (patch)
tree0ecad148d41060d9728486fd61309de6e8cb561e /src/source.sml
parentc5521a5f402e3d5f7c2e9c4a36966df196a70fdd (diff)
Initial support for reusing elaboration results
Diffstat (limited to 'src/source.sml')
-rw-r--r--src/source.sml4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/source.sml b/src/source.sml
index b85384ab..ce29904d 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -154,8 +154,8 @@ datatype decl' =
| DVal of string * con option * exp
| DValRec of (string * con option * exp) list
| DSgn of string * sgn
- | DStr of string * sgn option * str
- | DFfiStr of string * sgn
+ | DStr of string * sgn option * Time.time option * str
+ | DFfiStr of string * sgn * Time.time
| DOpen of string * string list
| DConstraint of con * con
| DOpenConstraints of string * string list