2008/5/14 Ulf Norell <ulfn at cs.chalmers.se>: > > I changed --no-universe-check to --type-in-type and changed the semantics to > the real thing. Nice. Do you have any plans for an "Agda commentary", to make it easier for the rest of us to implement features like this one? -- /NAD