From 25b0685cefe772c73562665a4cc8d2d40e5ff600 Mon Sep 17 00:00:00 2001
From: Simon Van Casteren <simon.van.casteren@gmail.com>
Date: Wed, 11 Dec 2019 13:58:01 +0100
Subject: Use elabFile completely instead of rebuilding it partially

---
 src/elaborate.sml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'src/elaborate.sml')

diff --git a/src/elaborate.sml b/src/elaborate.sml
index d5e190fa..85234775 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -4760,7 +4760,7 @@ and elabStr (env, denv) (str, loc) =
 
 fun resolveClass env = E.resolveClass (hnormCon env) (consEq env dummy) env
 
-fun elabFile basis basis_tm topStr topSgn top_tm env file =
+fun elabFile basis basis_tm topStr topSgn top_tm env changeEnv file =
     let
         val () = ModDb.snapshot ()
         val () = ErrorMsg.resetStructureTracker ()
@@ -4857,6 +4857,8 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file =
 
         val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn}
 
+        val env' = changeEnv env'
+
         fun elabDecl' x =
             (resetKunif ();
              resetCunif ();
-- 
cgit v1.2.3