summaryrefslogtreecommitdiff
path: root/src/sources
diff options
context:
space:
mode:
authorGravatar FrigoEU <simon.van.casteren@gmail.com>2019-07-31 15:13:18 +0200
committerGravatar FrigoEU <simon.van.casteren@gmail.com>2019-07-31 15:13:18 +0200
commit80e7bb6165a5ad6517b35f301228f56b58eef39c (patch)
treed9f3b42b6cb74ebacc43d4081e5d91aebbe7a20f /src/sources
parent83bab4581d9570e151b23db3b4de016600afa76d (diff)
first iteration of "typeOf" command
Diffstat (limited to 'src/sources')
-rw-r--r--src/sources3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/sources b/src/sources
index 851cdc16..e25ccd2e 100644
--- a/src/sources
+++ b/src/sources
@@ -69,6 +69,9 @@ $(SRC)/elab.sml
$(SRC)/elab_util.sig
$(SRC)/elab_util.sml
+$(SRC)/elab_util_pos.sig
+$(SRC)/elab_util_pos.sml
+
$(SRC)/elab_env.sig
$(SRC)/elab_env.sml