broke mathlib

Stream: general

[Paul-Nicolas Madelaine]

Hi everyone,

I'm was working on fixing a problem with the norm_cast tactic, and it seems like I broke something in data/list.
The thing is, this part of the code doesn't use norm_cast, and doesn't seem to use coercion at all for that matter.
Plus, the error messages I get are about the equation compiler and pattern matching.
Could someone take a look and help me figure out what I'm looking at?
Here is the incriminated commit: https://github.com/leanprover-community/mathlib/pull/1103/commits/4daf46595da984c2947a771d269e9acd64b0afc1

[Paul-Nicolas Madelaine]

I created a dedicated thread in 'PR reviews', it seems more appropriate than the general stream