summaryrefslogtreecommitdiff
path: root/src/elaborate.sig
diff options
context:
space:
mode:
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