[Jweb_Guru]

Pierre Pedrot has been very vocal in his belief that broken SR from coinductive types is a serious problem with Coq that needs to be fixed. This is quite different from introducing stuff that deliberately breaks it.