necessary type constraint?

[affeldt-aist]

https://github.com/math-comp/analysis/blob/9d80a0fbeeaa079a930c436d3d5dbb878491cf73/theories/lebesgue_measure.v#L829-L830

Removing : set R causes a stack overflow that is not explained yet.

There are more instances below in the file.

For the record. @CohenCyril @gares