[Agda] Is it possible to switch off universes checking?

[Andrés Sicard-Ramírez]

On 29 December 2015 at 18:46, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
> On 28/12/15 19:09, Nils Anders Danielsson wrote:
>> I don't know why universe polymorphism and --type-in-type cannot be used
>> together.
>
> I would be lovely if they could be used together.

I created a branch allowing type in type and universe polymorphism.
You can get it using

  $ git clone https://github.com/agda/agda.git
  $ cd agda
  $ git checkout issue-1764-maint
  $ make install-bin

Enjoy,

-- 
Andrés