idris-lang/Idris-dev — pull request #1496 by edwinb (2014-08-28 14:13:24+00:00)
Title: Postulate deceq

Just removing a couple of needless restrictions which don't affect sharing. There's no need to check inside types for unique type usage, or in pattern LHSs.