On Fri, Mar 8, 2013 at 2:23 PM, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote: > Moreover, it would be good to have a pragma MLTT that doesn't allow any > feature that take us beyond core MLTT (whatever we take that to be). +1 -- Andrés