summaryrefslogtreecommitdiff
path: root/src/sources
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-08-08 17:55:51 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-08-08 17:55:51 -0400
commitb9b67597324deb6e6dfc8ef33c60c110abc2af7b (patch)
tree2ff5f7417692c2590916a6eeb55aa38bbb47516f /src/sources
parente2a9136ed7123cb8e5cac4a20cbce5467643ecd6 (diff)
Specialization of single-parameter datatypes
Diffstat (limited to 'src/sources')
-rw-r--r--src/sources6
1 files changed, 6 insertions, 0 deletions
diff --git a/src/sources b/src/sources
index 23379bf4..94c37050 100644
--- a/src/sources
+++ b/src/sources
@@ -4,6 +4,9 @@ search.sml
list_util.sig
list_util.sml
+order.sig
+order.sml
+
errormsg.sig
errormsg.sml
@@ -75,6 +78,9 @@ reduce.sml
shake.sig
shake.sml
+specialize.sig
+specialize.sml
+
tag.sig
tag.sml