mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-21 22:17:19 +03:00
f09605b3dd
Fixes #2217 by demanding that global names in TT terms be unambiguous. The elaborator will always produce them that way, but user elab scripts might not, which led to confusion. Also, disentagle 'apply' and 'fill'. |
||
---|---|---|
.. | ||
expected | ||
reg035.idr | ||
reg035a.lidr | ||
reg035b.idr | ||
run |