summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2013-10-17 09:22:38 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2013-10-17 09:22:38 -0400
commit65b818146effe2f74192a3b1d65b4ec792a8a350 (patch)
treed21b187c3b5c3a63ba22408fada36d9871309be4 /src
parentd05e9343cbe1545602527e999e203c35f40d152a (diff)
Save disjointness environments across top-level declarations
Diffstat (limited to 'src')
-rw-r--r--src/elaborate.sml15
1 files changed, 6 insertions, 9 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index ace7a758..ff5a3b95 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -4002,6 +4002,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
end
val (env', n) = E.pushStrNamed env x sgn'
+
val denv' =
case #1 str' of
L'.StrConst _ => dopenConstraints (loc, env', denv) {str = x, strs = []}
@@ -4581,16 +4582,12 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file =
val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn}
- fun elabDecl' (d, (env, gs)) =
- let
- val () = resetKunif ()
- val () = resetCunif ()
- val (ds, (env', _, gs)) = elabDecl (d, (env, D.empty, gs))
- in
- (ds, (env', gs))
- end
+ fun elabDecl' x =
+ (resetKunif ();
+ resetCunif ();
+ elabDecl x)
- val (file, (env'', gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file
+ val (file, (env'', _, gs)) = ListUtil.foldlMapConcat elabDecl' (env', D.empty, []) file
fun oneSummaryRound () =
if ErrorMsg.anyErrors () then