zero in subring

Stream: maths

[Patrick Massot]

I just added to the perfectoid project:

instance subring_has_zero (R : Type*) [comm_ring R] (S : set R) [HS : is_subring S] : has_zero S :=
⟨⟨0, is_add_submonoid.zero_mem S⟩⟩

It seems this used to be unnecessary. Any idea what happened? Trying apply_instance loops forever