summaryrefslogtreecommitdiff
path: root/src/elaborate.sig
diff options
context:
space:
mode:
authorGravatar FrigoEU <simon.van.casteren@gmail.com>2019-08-01 17:38:09 +0200
committerGravatar FrigoEU <simon.van.casteren@gmail.com>2019-08-01 17:38:09 +0200
commit0e520d3fd675bcebb5751bd1a0c304033f4f7782 (patch)
treedf82ceca2d92dd8261fc7884438479ab576d6d53 /src/elaborate.sig
parent9e2b026fea11ae89a53d4fc1c674ef8e43b2c2ce (diff)
Improved typeOf searching and handling of Top and Basis
Diffstat (limited to 'src/elaborate.sig')
-rw-r--r--src/elaborate.sig6
1 files changed, 6 insertions, 0 deletions
diff --git a/src/elaborate.sig b/src/elaborate.sig
index d60cff42..03359814 100644
--- a/src/elaborate.sig
+++ b/src/elaborate.sig
@@ -47,4 +47,10 @@ signature ELABORATE = sig
val incremental : bool ref
val verbose : bool ref
+ val dopen: ElabEnv.env
+ -> { str: int
+ , strs: string list
+ , sgn: Elab.sgn }
+ -> (Elab.decl list * ElabEnv.env)
+
end