summaryrefslogtreecommitdiff
path: root/src/sources
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-01-26 15:29:09 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-01-26 15:29:09 -0500
commit95beeda12defe36c4d4df42d3dee3bd753e19ff5 (patch)
tree6c9203f55fc835de1bbf15e9c3c92bedf40c59aa /src/sources
parente0a8e775a4c1e12debb2a3fa458007340685dc9d (diff)
Rename Laconic* modules to Source*
Diffstat (limited to 'src/sources')
-rw-r--r--src/sources6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/sources b/src/sources
index e82c0c7e..9c879139 100644
--- a/src/sources
+++ b/src/sources
@@ -1,7 +1,7 @@
errormsg.sig
errormsg.sml
-laconic.sml
+source.sml
lacweb.grm
lacweb.lex
@@ -9,8 +9,8 @@ lacweb.lex
print.sig
print.sml
-laconic_print.sig
-laconic_print.sml
+source_print.sig
+source_print.sml
elab.sml