[ deriving Eq ] compute incompatible constructors
added Tactic.Deriving.Eq to test/Main.agda
added level polymorphic version of the empty type
Merge branch 'compat-2.4.0'