summaryrefslogtreecommitdiff
path: root/src/elaborate.sig
diff options
context:
space:
mode:
Diffstat (limited to 'src/elaborate.sig')
-rw-r--r--src/elaborate.sig14
1 files changed, 14 insertions, 0 deletions
diff --git a/src/elaborate.sig b/src/elaborate.sig
index 03359814..88ea068f 100644
--- a/src/elaborate.sig
+++ b/src/elaborate.sig
@@ -53,4 +53,18 @@ signature ELABORATE = sig
, sgn: Elab.sgn }
-> (Elab.decl list * ElabEnv.env)
+ val elabSgn: (ElabEnv.env * Disjoint.env)
+ -> Source.sgn
+ -> (Elab.sgn * Disjoint.goal list)
+
+ datatype constraint =
+ Disjoint of Disjoint.goal
+ | TypeClass of ElabEnv.env * Elab.con * Elab.exp option ref * ErrorMsg.span
+
+ val elabStr: (ElabEnv.env * Disjoint.env)
+ -> Source.str
+ -> (Elab.str * Elab.sgn * constraint list)
+
+ val subSgn: ElabEnv.env -> ErrorMsg.span -> Elab.sgn -> Elab.sgn -> unit
+
end