On 16 February 2016 at 08:33, Andrés Sicard-Ramírez <asr at eafit.edu.co> wrote: > I got the full normalised types with 2.4.2.5 without using C-u C-u. I > need to make some tests to clear up confusion... I filed issue https://github.com/agda/agda/issues/1851 . -- Andrés