[Agda] C-c C-c turns issue 64 into a bug

Samuel Bronson naesten at gmail.com
Fri May 16 15:37:45 CEST 2008


Previously, http://code.google.com/p/agda/issues/detail?id=64 has been
simply an annoying infelicity... but with C-c C-c, it becomes a bug:
printing names as if they are not in scope when they are does not
produce valid code. (It wouldn't produce valid code if the names were
actually out of scope, either, but that can't be helped ;-)


More information about the Agda mailing list