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
commite75a028e3ced5d05be1baa05c6fb1a83b277a45f (patch)
tree3b71b2a102795dcd3b2bb3e106a0ee2309487376 /src/elaborate.sig
parent4e0410306a4d4288dd36450dc8f9ea2e8bd0a154 (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