diff options
| author |  Simon Van Casteren <simon.van.casteren@gmail.com> | 2019-12-11 13:58:01 +0100 |
|---|---|---|
| committer |  Simon Van Casteren <simonvancasteren@localhost.localdomain> | 2019-12-13 11:46:57 +0100 |
| commit | 25b0685cefe772c73562665a4cc8d2d40e5ff600 (patch) | |
| tree | d5b3b383267e8f44bb32881b04839623e3becee3 /src/elaborate.sml | |
| parent | a0efdaf11337df1fb1a5478f9a193a2737b2665b (diff) | |
Use elabFile completely instead of rebuilding it partially
Diffstat (limited to 'src/elaborate.sml')
| -rw-r--r-- | src/elaborate.sml | 4 |
1 files changed, 3 insertions, 1 deletions
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 (); |