edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2025-01-05 03:17:21 +03:00
Code Issues Projects Releases Wiki Activity

Clear delayed holes on failure

Browse Source
This commit is contained in:
Edwin Brady 2019-05-12 16:32:56 +01:00
parent 14f717aa33
commit 9baf180127
1 changed files with 5 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/TTImp/Elab.idr
View File

@ -50,9 +50,11 @@ elabTerm defining mode env tm ty
solveConstraints solvemode Normal solveConstraints solvemode Normal
logTerm 5 "Looking for delayed in " chktm logTerm 5 "Looking for delayed in " chktm
ust <- get UST ust <- get UST
retryDelayed (delayedElab ust) catch (retryDelayed (delayedElab ust))
ust <- get UST (\err =>
put UST (record { delayedElab = [] } ust) do ust <- get UST
put UST (record { delayedElab = [] } ust)
throw err)
-- As long as we're not in a case block, finish off constraint solving -- As long as we're not in a case block, finish off constraint solving
when (not incase) $ when (not incase) $
-- resolve any default hints -- resolve any default hints