summaryrefslogtreecommitdiff
path: root/src/elaborate.sig
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-08-07 16:53:06 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2011-08-07 16:53:06 -0400
commit2db0b84897793a6367595b8ed6ba2e1eaa3b76d5 (patch)
tree3b71b2a102795dcd3b2bb3e106a0ee2309487376 /src/elaborate.sig
parentc1ff87c8dc39e9c5b550ef6969c0c16b7888f8e6 (diff)
'-dumpTypes'
Diffstat (limited to 'src/elaborate.sig')
-rw-r--r--src/elaborate.sig4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/elaborate.sig b/src/elaborate.sig
index 0dbf36e3..6d1583a4 100644
--- a/src/elaborate.sig
+++ b/src/elaborate.sig
@@ -32,4 +32,8 @@ signature ELABORATE = sig
val resolveClass : ElabEnv.env -> Elab.con -> Elab.exp option
+ val dumpTypes : bool ref
+ (* After elaboration (successful or failed), should I output a mapping from
+ * all identifiers to their kinds/types? *)
+
end