On 5 March 2015 at 12:56, Sergei Meshveliani <mechvel at botik.ru> wrote: > If it is obsolete, then Agda probably needs to report this explicitly. I was wrong. The option is not obsolete. -- Andrés