summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-05-31 15:25:27 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-05-31 15:25:27 -0400
commitbecba29a1753db244749e87ba13eebd1be401ef6 (patch)
tree61ba05a318cb4993f095c2ab959a78cb68291471 /src
parent8c06af6123389e9f4a2302e08230b1e5aaadb590 (diff)
Expose resolveClass from Elaborate
Diffstat (limited to 'src')
-rw-r--r--src/elaborate.sig2
-rw-r--r--src/elaborate.sml6
2 files changed, 6 insertions, 2 deletions
diff --git a/src/elaborate.sig b/src/elaborate.sig
index cab3c3c5..0dbf36e3 100644
--- a/src/elaborate.sig
+++ b/src/elaborate.sig
@@ -30,4 +30,6 @@ signature ELABORATE = sig
val elabFile : Source.sgn_item list -> Source.decl list -> Source.sgn_item list
-> ElabEnv.env -> Source.file -> Elab.file
+ val resolveClass : ElabEnv.env -> Elab.con -> Elab.exp option
+
end
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 961c2b2e..62d99bf3 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -3763,6 +3763,8 @@ and elabStr (env, denv) (str, loc) =
(strerror, sgnerror, []))
end
+fun resolveClass env = E.resolveClass (hnormCon env) (consEq env) env
+
fun elabFile basis topStr topSgn env file =
let
val () = mayDelay := true
@@ -3815,7 +3817,7 @@ fun elabFile basis topStr topSgn env file =
let
val c = normClassKey env c
in
- case E.resolveClass (hnormCon env) (consEq env) env c of
+ case resolveClass env c of
SOME e => r := SOME e
| NONE => expError env (Unresolvable (loc, c))
end) gs
@@ -3888,7 +3890,7 @@ fun elabFile basis topStr topSgn env file =
val c = normClassKey env c
in
- case E.resolveClass (hnormCon env) (consEq env) env c of
+ case resolveClass env c of
SOME e => (r := SOME e;
(NONE, true))
| NONE =>