[Agda] --termination-depth

Andrés Sicard-Ramírez asr at eafit.edu.co
Thu Mar 5 21:01:22 CET 2015


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


More information about the Agda mailing list