search

edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
902 stars 58 forks source link

'using' multiple named instances in scope fix #314

Closed MarcelineVQ closed 4 years ago

MarcelineVQ commented 4 years ago

Change where the open hints is snapshotted. This is done too late, causing named implementations to remain in scope. addressing https://github.com/edwinb/Idris2/issues/307 caused by the reordering in https://github.com/edwinb/Idris2/commit/d39c701f280c4ca46f9ca2ba36b59eea3958277d

edwinb commented 4 years ago

Ah yes, I missed that, thanks!