On 2010-12-30 17:24, Thorsten Altenkirch wrote: > Not true. The new mechanism using \infty, \sharp and \fat was > initially implemented on top of the old one and hence these issues are > not related to the alleged coup. Thorsten is right, see the following message: Changes to coinduction http://article.gmane.org/gmane.comp.lang.agda/763/ -- /NAD